Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Conditional Simple Temporal Networks with Uncertainty and Resources
Authors: Carlo Combi, Roberto Posenato, Luca Viganò, Matteo Zavatteri
JAIR 2019 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | As a proof-of-concept, we wrote the specification of the TGA encoding the CSTNUR depicted in Figure 6 and ran Uppaal-TIGA to answer to the decision problem of dynamic controllability (Zavatteri, 2019).We took advantage of Boolean variables to represent propositions and the RA relation6. We used a Free BSD virtual machine running on top of a VMWare ESXi using a physical machine equipped with an Intel i7 2.80GHz and 20GB of RAM for the experimental evaluation. The VM was assigned 16GB of RAM7 and full CPU power. We verified that the CSTNUR in Figure 6 is dynamically controllable. The model checking phase took 207 minutes and 28 seconds to synthesize a 1.6MB memoryless execution strategy as a certificate of YES for this decision problem. |
| Researcher Affiliation | Academia | Carlo Combi EMAIL Dipartimento di Informatica, Università di Verona strada le grazie 15, 37134 Verona, Italy Roberto Posenato EMAIL Dipartimento di Informatica, Università di Verona strada le grazie 15, 37134 Verona, Italy Luca Viganò EMAIL Department of Informatics, King s College London 30 Aldwych, London E7 9QU, United Kingdom Matteo Zavatteri EMAIL Dipartimento di Informatica, Università di Verona strada le grazie 15, 37134 Verona, Italy |
| Pseudocode | No | The paper describes methods and encodings using mathematical definitions, diagrams (e.g., Figures 7, 8, 9, 10 for TGA patterns), and prose. It does not contain any clearly labeled 'Pseudocode' or 'Algorithm' blocks with structured steps. |
| Open Source Code | Yes | Zavatteri, M. (2019). Example of a CSTNUR encoded as TGA. http://regis.di.univr.it/Flight Example.tar.bz2. |
| Open Datasets | No | The paper uses a 'real-world motivating example representing a round-trip flight process' which is a constructed scenario described in detail in Section 2. It does not refer to or provide access information for any pre-existing public datasets used for empirical evaluation. |
| Dataset Splits | No | The paper uses a motivating example for its analysis and proof-of-concept. It does not involve empirical evaluation on a dataset that would require training/test/validation splits. |
| Hardware Specification | Yes | We used a Free BSD virtual machine running on top of a VMWare ESXi using a physical machine equipped with an Intel i7 2.80GHz and 20GB of RAM for the experimental evaluation. The VM was assigned 16GB of RAM7 and full CPU power. |
| Software Dependencies | No | Uppaal-TIGA is an extension of Uppaal implementing the first efficient on-the-fly algorithm for solving games based on TGAs with respect to reachability and safety properties (Behrmann et al., 2007). As a proof-of-concept, we wrote the specification of the TGA encoding the CSTNUR depicted in Figure 6 and ran Uppaal-TIGA to answer to the decision problem of dynamic controllability (Zavatteri, 2019). |
| Experiment Setup | No | The paper mentions the outcome of the model checking phase: 'The model checking phase took 207 minutes and 28 seconds to synthesize a 1.6MB memoryless execution strategy'. However, it does not specify any setup details such as hyperparameters, optimizer settings, or configuration parameters for the Uppaal-TIGA run itself, beyond mentioning the hardware. |