Is your model checker on time? On the complexity of model checking for timed modal logics
From MaRDI portal
Publication:1858436
DOI10.1016/S1567-8326(02)00022-XzbMath1008.68030OpenAlexW2057980886MaRDI QIDQ1858436
Luca Aceto, François Laroussinie
Publication date: 13 February 2003
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s1567-8326(02)00022-x
Related Items (9)
Efficient timed model checking for discrete-time systems ⋮ State explosion in almost-sure probabilistic reachability ⋮ The tail-recursive fragment of timed recursive CTL ⋮ The power of reachability testing for timed automata ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets ⋮ When are timed automata weakly timed bisimilar to time Petri nets? ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ Timed network games
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Interval logics and their decision procedures. II: A real-time interval logic
- Minimum and maximum delay problems in real-time systems
- Model-checking in dense real-time
- Real-time logics: Complexity and expressiveness
- Results on the propositional \(\mu\)-calculus
- A linear algorithm to solve fixed-point equations on transition systems
- A calculus of durations
- Computer aided verification. 5th international conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993. Proceedings
- A theory of timed automata
- Model checking and boolean graphs
- Symbolic model checking for real-time systems
- CAV '94, Computer aided verification. 6th International Conference, Stanford, CA, USA, June 21--23, 1994. Proceedings
- Reasoning about infinite computations
- Complexity of equivalence problems for concurrent systems of finite agents
- Symbolic model checking for \(\mu\)-calculus requires exponential time
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- HyTech: A model checker for hybrid systems
- Kronos: A verification tool for real-time systems
- Uppaal in a nutshell
- Automated verification of an audio-control protocol using UPPAAL
- Relationships between nondeterministic and deterministic tape complexities
- A lattice-theoretical fixpoint theorem and its applications
- Characteristic Formulae for Timed Automata
- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
- From timed automata to logic — and back
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Graph-Based Algorithms for Boolean Function Manipulation
- Algebraic laws for nondeterminism and concurrency
- The complexity of propositional linear temporal logics
- Alternation
- A really temporal logic
- On the power of bounded concurrency I
- The benefits of relaxing punctuality
- Model-checking for real-time systems
- An automata-theoretic approach to branching-time model checking
- On model checking for the \(\mu\)-calculus and its fragments
- On the complexity of verifying concurrent transition systems
This page was built for publication: Is your model checker on time? On the complexity of model checking for timed modal logics
