Static guard analysis in timed automata verification

DOI10.1007/3-540-36577-X_18MaRDI QIDQ4417927zbMATH OpenFDO

Authors Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim G. Larsen

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2619/26190254.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Tools and Algorithms for the Construction and Analysis of Systems
• Better abstractions for timed automata
• Better abstractions for timed automata
• Analysis of timed systems using time-abstracting bisimulations
• Difference bound constraint abstraction for timed automata reachability checking

Cited in

(22)

• Static analysis for state-space reductions preserving temporal logics
• Updatable timed automata
• Certifying emptiness of timed Büchi automata
• Zone-based verification of timed automata: extrapolations, simulations and what next?
• Configurable verification of timed automata with discrete variables
• Untangling the graphs of timed automata to decrease the number of clocks
• A partial order semantics approach to the clock explosion problem of timed automata
• Model Checking Real-Time Systems
• Better abstractions for timed automata
• Speeding up model checking of timed-models by combining scenario specialization and live component analysis
• Checking timed Büchi automata emptiness using LU-abstractions
• Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras
• Verified certification of reachability checking for timed automata
• Finding minimum and maximum termination time of timed automata models with cyclic behaviour
• Tools and Algorithms for the Construction and Analysis of Systems
• Lazy Reachability Checking for Timed Automata with Discrete Variables
• An efficient state space construction for a class of timed automata
• Reachability for updatable timed automata made faster and more effective
• Timed automata verification and synthesis via finite automata learning
• On-the-fly symbolic algorithm for timed ATL with abstractions
• An integer static analysis for better extrapolation in Uppaal
• Accelerating worst case execution time analysis of timed automata models with cyclic behaviour

Describes a project that uses

Uses Software

• Uppaal
• CMC

This page was built for publication: Static guard analysis in timed automata verification

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