Model Checking Timed Automata with Priorities Using DBM Subtraction

DOI10.1007/11867340_10zbMATH Open1141.68462OpenAlexW1914485921MaRDI QIDQ3511228FDOQ3511228

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

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

Mathematics Subject Classification ID

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

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

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)