Model Checking Timed Automata with Priorities Using DBM Subtraction

DOI10.1007/11867340_10MaRDI QIDQ3511228zbMATH OpenOpenAlexFDO

Authors Alexandre David, John Håkansson, Paul Pettersson, Kim G. Larsen

Publication date 8 July 2008

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

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.4049

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated Technology for Verification and Analysis
• A quadratic-time DBM-based successor algorithm for checking timed automata
• Hypervolume Approximation in Timed Automata Model Checking
• scientific article; zbMATH DE number 1507209
• scientific article; zbMATH DE number 2102690

Cited in

(5)

• Improving the construction of the DBM over-approximation of the state space of real-time preemptive systems
• Shrinking timed automata
• Model Checking Bounded Prioritized Time Petri Nets
• Automated Technology for Verification and Analysis
• A quadratic-time DBM-based successor algorithm for checking timed automata

Describes a project that uses

Uses Software

• Uppaal

This page was built for publication: Model Checking Timed Automata with Priorities Using DBM Subtraction

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