Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness
Authors: Giuseppe De Giacomo, Riccardo De Masellis, Marco Montali
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We define a necessary and sufficient condition to characterize whether an LTLf formula is insensitive to infiniteness, which can be automatically checked by any LTL reasoner. Then, we show that typical LTLf specification patterns used in process and service modeling in CS, as well as trajectory constraints in Planning and transition-based LTLf specifications of action domains in KR, are indeed very often insensitive to infiniteness. As a further contribution, we give a simple direct algorithm for computing such NFA. The theorem can be proven automatically, making use of an LTL reasoner on infinite traces. Specifically, each DECLARE pattern can be grounded on a concrete set of tasks (propositions), and then, by Theorem 4, we simply need to check the validity of the corresponding formula. In fact, we encoded each validity check in the model checker Nu SMV2, following the approach of satisfiability via model checking (Rozier and Vardi 2007). Nu SMV confirmed that all patterns but the negation chain succession are insensitive to infiniteness. |
| Researcher Affiliation | Academia | Giuseppe De Giacomo Riccardo De Masellis Dip. di Ing. Informatica, Automatica e Gestionale Sapienza Universit a di Roma, Italy {degiacomo,demasellis}@dis.uniroma1.it Marco Montali KRDB Research Centre for Knowledge and Data Free University of Bozen-Bolzano, Italy montali@inf.unibz.it |
| Pseudocode | Yes | 1: algorithm LTLf 2NFA() 2: input LTLf formula ϕ 3: output NFA Aϕ = (2P, S, {s0}, ϱ, {sf}) |
| Open Source Code | Yes | The full list of specifications is available here: http://www.inf.unibz.it/ montali/AAAI14 |
| Open Datasets | No | The paper is theoretical and does not use or refer to publicly available datasets for training or evaluation in the traditional sense. It analyzes logical formulas and patterns. |
| Dataset Splits | No | The paper is theoretical and does not involve empirical experiments with datasets that would require training, validation, or test splits. |
| Hardware Specification | No | The paper is theoretical and does not specify any hardware used for its analysis or verification processes. |
| Software Dependencies | No | The paper mentions the use of 'the model checker Nu SMV' but does not specify its version number. |
| Experiment Setup | Yes | E.g., the following Nu SMV specification checks whether response is insensitive to infiniteness: MODULE main VAR a:boolean; b:boolean; other:boolean; end:boolean; LTLSPEC (F(end) & G(end -> X(end)) & G(end -> (!b & !a))) -> ( (G(a -> X(F(b)))) <-> (G((a -> (X((F(b & !end))) & !end)) | end)) ) |