On expressiveness and complexity in real-time model checking

On expressiveness and complexity in real-time model checking

Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called punctual specifications. In this paper we introduce a significantly more expr...

Full description

Bibliographic Details
Main Authors:	Bouyer, P, Markey, N, Ouaknine, J, Worrell, J
Format:	Journal article
Language:	English
Published:	2008

Similar Items

Real-time model checking: Algorithms and complexity
by: Worrell, J, et al.
Published: (2008)

The cost of punctuality
by: Bouyer, P, et al.
Published: (2007)

Branching-time model checking of parametric one-counter automata
by: Göller, S, et al.
Published: (2012)

Branching−Time Model Checking of Parametric One−Counter Automata
by: Göller, S, et al.
Published: (2012)

Model Checking One-clock Priced Timed Automata
by: Patricia Bouyer, et al.
Published: (2008-06-01)

On termination for faulty channel machines
by: Bouyer, P, et al.
Published: (2008)

On termination and invariance for faulty channel machines
by: Bouyer, P, et al.
Published: (2012)

Computing Rational Radical Sums in Uniform TC0
by: Hunter, P, et al.
Published: (2010)

Computing Rational Radical Sums in Uniform TC0
by: Hunter, P, et al.
Published: (2010)

Algebraic model checking for discrete linear dynamical systems
by: Luca, F, et al.
Published: (2022)

On the Magnitude of Completeness Thresholds in Bounded Model Checking
by: Bundala, D, et al.
Published: (2012)

On LTL model-checking for low-dimensional discrete linear dynamical systems
by: Karimov, T, et al.
Published: (2020)

Model Checking Succinct and Parametric One-Counter Automata.
by: Göller, S, et al.
Published: (2010)

Model Checking Succinct and Parametric One−Counter Automata
by: Göller, S, et al.
Published: (2010)

Linear Completeness Thresholds for Bounded Model Checking.
by: Kroening, D, et al.
Published: (2011)

Model checking Timed CSP
by: Armstrong, P, et al.
Published: (2012)

Completeness and Complexity of Bounded Model Checking
by: Clarke, E, et al.
Published: (2004)

Model checking flat freeze LTL on one-counter automata
by: Lechner, A, et al.
Published: (2016)

Parallel assignments in software model checking
by: Ouaknine, J
Published: (2006)

Model Checking Flat Freeze LTL on One-Counter Automata
by: Antonia Lechner, et al.
Published: (2018-12-01)

Decidability and complexity results for timed automata via channel machines
by: Abdulla, P, et al.
Published: (2005)

ON THE DECIDABILITY AND COMPLEXITY OF METRIC TEMPORAL LOGIC OVER FINITE WORDS
by: Ouaknine, J, et al.
Published: (2007)

Towards a Theory of Time-Bounded Verification.
by: Ouaknine, J, et al.
Published: (2010)

On the complexity of the orbit problem
by: Chonev, V, et al.
Published: (2016)

On the complexity of the orbit problem
by: Chonev, V, et al.
Published: (2016)

Computational challenges in bounded model checking.
by: Clarke, E, et al.
Published: (2005)

Computational Challenges in Bounded Model Checking
by: Clarke, E, et al.
Published: (2015)

Computational challenges in bounded model checking
by: Clarke, E, et al.
Published: (2005)

Exact acceleration of complex real-time model checking based on overlapping cycle
by: Guoqing Wang, et al.
Published: (2020-05-01)

Undecidability of universality for timed automata with minimal resources
by: Adams, S, et al.
Published: (2007)

Undecidability of Universality for Timed Automata with Minimal Resources
by: Adams, S, et al.
Published: (2007)

Real-Time Model-Checking: Parameters everywhere
by: Veronique Bruyere, et al.
Published: (2007-02-01)

Time-Bounded Verification
by: Ouaknine, J, et al.
Published: (2009)

LTL model checking of interval Markov chains
by: Benedikt, M, et al.
Published: (2013)

On the decidability and complexity of Metric Temporal Logic over finite words
by: Joel Ouaknine, et al.
Published: (2007-02-01)

Efficient CTMC Model Checking of Linear Real−Time Objectives
by: Barbot, B, et al.
Published: (2011)

On the relationship between reachability problems in timed and counter automata
by: Haase, C, et al.
Published: (2012)

On the Relationship between Reachability Problems in Timed and Counter Automata
by: Haase, C, et al.
Published: (2012)

Alternating Timed Automata over Bounded Time
by: Jenkins, M, et al.
Published: (2010)

Trace Checking with Real−Time Specifications
by: Deutschmann, R, et al.
Published: (2004)