Checking interval properties of computations

DOI10.1007/S00236-015-0250-1zbMATH Open1350.68184arXiv1601.03195OpenAlexW2952938415MaRDI QIDQ329413FDOQ329413

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)

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.

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

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

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)

Cites Work

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

Cited In (25)

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

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)