Characteristic Formulae for Timed Automata
From MaRDI portal
Publication:2729632
DOI10.1051/ita:2000131zbMath0974.68121OpenAlexW2111205369MaRDI QIDQ2729632
Mikkel L. Pedersen, Jan Poulsen, Anna Ingólfsdóttir, Luca Aceto
Publication date: 23 July 2001
Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)
Full work available at URL: https://eudml.org/doc/222071
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (5)
Characteristic formulae for fixed-point semantics: a general framework ⋮ Bisimulation on speed: Lower time bounds ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ Non-Interference Control Synthesis for Security Timed Automata ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Results on the propositional \(\mu\)-calculus
- Determinacy \(\to\) (observation equivalence \(=\) trace equivalence)
- Characterizing finite Kripke structures in propositional temporal logic
- Bisimulation through probabilistic testing
- CONCUR '90. Theories of concurrency: unification and extension. Amsterdam, The Netherlands, August 1990. Proceedings
- A theory of timed automata
- Characteristic formulae for processes with divergence
- An efficiency preorder for processes
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- A lattice-theoretical fixpoint theorem and its applications
- From timed automata to logic — and back
- A modal characterization of observational congruence on finite terms of CCS
- Algebraic laws for nondeterminism and concurrency
- Formal verification of parallel programs
- Bisimulation can't be traced
This page was built for publication: Characteristic Formulae for Timed Automata
