A quadratic-time DBM-based successor algorithm for checking timed automata

DOI10.1016/J.IPL.2005.05.027MaRDI QIDQ1044715zbMATH OpenOpenAlexFDO

Authors Xuandong Li, Guoliang Zheng, Jian-hua Zhao

Publication date 18 December 2009

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2005.05.027

zbMATH Keywords

model checkingformal methodstimed automatondifference bound matrix

Mathematics Subject Classification ID

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

Recommendations

• Model Checking Timed Automata with Priorities Using DBM Subtraction
• Hypervolume Approximation in Timed Automata Model Checking
• Lectures on Concurrency and Petri Nets
• scientific article; zbMATH DE number 1507209
• Difference bound constraint abstraction for timed automata reachability checking

Cites work

• scientific article; zbMATH DE number 1962849 (Why is no real title available?)
• A theory of timed automata
• Formal Modeling and Analysis of Timed Systems
• Lectures on Concurrency and Petri Nets

Cited in

(6)

• Reachability in timed automata with diagonal constraints
• Improving the construction of the DBM over-approximation of the state space of real-time preemptive systems
• Simulations for event-clock automata
• Model Checking Timed Automata with Priorities Using DBM Subtraction
• Better abstractions for timed automata
• Finding minimum and maximum termination time of timed automata models with cyclic behaviour

Describes a project that uses

Uses Software

• Uppaal
• HyTech
• Kronos

This page was built for publication: A quadratic-time DBM-based successor algorithm for checking timed automata

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