Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy

DOI10.1016/j.ic.2018.09.006zbMath1400.68121OpenAlexW2891153460MaRDI QIDQ1784961

Adriano Peron, Angelo Montanari, Pietro Sala, Alberto Molinari, Laura Bozzelli

Publication date: 27 September 2018

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11390/1130801

zbMATH Keywords

computational complexitymodel checkinginterval temporal logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Complexity analysis of a unifying algorithm for model checking interval temporal logic, \textsc{Pspace}-completeness of the temporal logic of sub-intervals and suffixes, Interval Temporal Logic for Visibly Pushdown Systems, Unnamed Item, Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*

Uses Software

• MCMAS
• DPF
• DDVerify

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maintaining knowledge about temporal intervals
• Checking interval properties of computations
• Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
• More complicated questions about maxima and minima, and some closures of NP
• The temporal semantics of concurrent programs
• Intervals and tenses
• On truth-table reducibility to SAT
• The polynomial-time hierarchy
• Duration calculus. A formal approach to real-time systems.
• Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives
• The dark side of interval temporal logic: marking the undecidability border
• Expressiveness and completeness of an interval tense logic
• Temporal prepositions and their logic
• Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments
• Tableaux for Logics of Subinterval Structures over Dense Orderings
• A decidable weakening of Compass Logic based on cone-shaped cardinal directions
• Bounded Query Classes
• Counting CTL
• Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• A Modal Logic for Chopping Intervals
• A propositional modal logic of time intervals
• NP trees and Carnap's modal logic
• A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
• Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
• Satisfiability and model checking for the logic of sub-intervals under the homogeneity assumption
• An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions
• Model Checking Database Applications
• A Road Map of Interval Temporal Logics and Duration Calculi