Checking interval properties of computations

DOI10.1007/S00236-015-0250-1MaRDI QIDQ329413zbMATH OpenOpenAlexFDO

Authors Alberto Molinari, Angelo Montanari, Aniello Murano, Giuseppe Perelli, Adriano Peron

Publication date 21 October 2016

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.03195

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Abstract: Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over finite Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity.

Recommendations

• Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives
• Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
• Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy
• scientific article; zbMATH DE number 6767596
• Interval vs. point temporal logic model checking. An expressiveness comparison

Cites work

• scientific article; zbMATH DE number 1696444 (Why is no real title available?)
• scientific article; zbMATH DE number 5595151 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 6131597 (Why is no real title available?)
• A Modal Logic for Chopping Intervals
• A Road Map of Interval Temporal Logics and Duration Calculi
• A propositional modal logic of time intervals
• Checking interval properties of computations
• Decidability of model checking multi-agent systems against a class of EHS specifications
• Intervals and tenses
• Maintaining knowledge about temporal intervals
• Maximal decidable fragments of Halpern and Shoham's modal logic of intervals
• Model checking propositional dynamic logic with all extras
• Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
• SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
• Tableaux for logics of subinterval structures over dense orderings
• The complexity of propositional linear temporal logics
• The dark side of interval temporal logic: marking the undecidability border
• The temporal semantics of concurrent programs
• The undecidability of the logic of subintervals

Cited in

(25)

• Verification, Model Checking, and Abstract Interpretation
• Interval temporal logic model checking: the border between good and bad HS fragments
• Which fragments of the interval temporal logic HS are tractable in model checking?
• Model checking the logic of Allen's relations \textit{Meets} and \textit{Started-by} is \(\mathbf{P}^{\mathbf{NP}}\)-complete
• Decidability and complexity of the fragments of the modal logic of Allen's relations over the rationals
• Parametric interval temporal logic over infinite words
• Adding the relation \textit{Meets} to the temporal logic of prefixes and infixes makes it EXPSPACE-complete
• Constraining cycle alternations in model checking for interval temporal logic
• Interval Temporal Logic for Visibly Pushdown Systems
• Complexity analysis of a unifying algorithm for model checking interval temporal logic
• On a Temporal Logic of Prefixes and Infixes.
• Interval vs. point temporal logic model checking. An expressiveness comparison
• Interval analysis and automatic result verification
• Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy
• Evaluation of temporal datasets via interval temporal logic model checking
• Model checking interval temporal logics with regular expressions
• On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions
• \textsc{Pspace}-completeness of the temporal logic of sub-intervals and suffixes
• Checking interval properties of computations
• A separation theorem for discrete-time interval temporal logic
• An in-depth investigation of interval temporal logic model checking with regular expressions
• Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives
• On coarser interval temporal logics
• Extracting interval temporal logic rules: a first approach
• Allen-like theory of time for tree-like structures

This page was built for publication: Checking interval properties of computations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q329413)