The power of reachability testing for timed automata
From MaRDI portal
Publication:1399974
DOI10.1016/S0304-3975(02)00334-1zbMath1023.68060OpenAlexW1971949385MaRDI QIDQ1399974
Augusto Burgueño, Luca Aceto, Patricia Bouyer, Kim Guldstrand Larsen
Publication date: 30 July 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(02)00334-1
Related Items (14)
\textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability ⋮ How to stop time stopping ⋮ Model-checking timed automata with deadlines with Uppaal ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ Model checking duration calculus: a practical approach ⋮ Decomposition of timed automata for solving scheduling problems ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ On-the-fly \(TCTL\) model checking for time Petri nets ⋮ An Introduction to Timed Automata ⋮ A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata ⋮ Checking Timed Büchi Automata Emptiness Using LU-Abstractions ⋮ Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*
Uses Software
Cites Work
- Minimum and maximum delay problems in real-time systems
- Model-checking in dense real-time
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- Bisimulation through probabilistic testing
- A theory of timed automata
- Characteristic formulae for processes with divergence
- Testing equivalences for processes
- Frontier between decidability and undecidability: A survey
- HyTech: A model checker for hybrid systems
- Kronos: A verification tool for real-time systems
- Uppaal in a nutshell
- Is your model checker on time? On the complexity of model checking for timed modal logics
- A lattice-theoretical fixpoint theorem and its applications
- From timed automata to logic — and back
- Compositionality Through an Operational Semantics of Contexts
- Quantales, observational logic and process semantics
- Bisimulation can't be traced
- On the Forms of the Predicates in the Theory of Constructive Ordinals
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The power of reachability testing for timed automata
