Characteristic formulae for timed autoamta

DOI10.1051/ITA:2000131MaRDI QIDQ2729632zbMATH OpenOpenAlexFDO

Authors Luca Aceto, Anna Ingolfsdottir, Mikkel L. Pedersen, Jan Poulsen

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

zbMATH Keywords

real-time logictimed bisimulation equivalence

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• From timed automata to logic -- and back
• On characteristic formulae for event-recording automata
• scientific article; zbMATH DE number 2102690
• A theory of timed automata
• Compositional methods in characterization of timed event structures

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• A modal characterization of observational congruence on finite terms of CCS
• A theory of timed automata
• Algebraic laws for nondeterminism and concurrency
• An efficiency preorder for processes
• Bisimulation can't be traced
• Bisimulation through probabilistic testing
• Characteristic formulae for processes with divergence
• Characterizing finite Kripke structures in propositional temporal logic
• CONCUR '90. Theories of concurrency: unification and extension. Amsterdam, The Netherlands, August 1990. Proceedings
• Determinacy \(\to\) (observation equivalence \(=\) trace equivalence)
• Formal verification of parallel programs
• From timed automata to logic -- and back
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 176729 (Why is no real title available?)
• scientific article; zbMATH DE number 1512618 (Why is no real title available?)
• scientific article; zbMATH DE number 1418333 (Why is no real title available?)
• Results on the propositional \(\mu\)-calculus

Cited in

(10)

• Axiomatising timed automata
• Is your model checker on time? On the complexity of model checking for timed modal logics
• When are prime formulae characteristic?
• On characteristic formulae for event-recording automata
• Non-interference control synthesis for security timed automata
• Characteristic formulae for fixed-point semantics: a general framework
• Compositional methods in characterization of timed event structures
• From timed automata to logic -- and back
• Bisimulation on speed: Lower time bounds
• Timed modal logics for real-time systems. Specification, verification and control

Describes a project that uses

Uses Software

• CMC

This page was built for publication: Characteristic formulae for timed autoamta

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2729632)