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

DOI10.1016/j.ipl.2005.05.027zbMath1184.68335OpenAlexW2046894268MaRDI QIDQ1044715

Guoliang Zheng, Xuandong Li, 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)

Related Items (3)

Better abstractions for timed automata ⋮ Unnamed Item ⋮ Finding minimum and maximum termination time of timed automata models with cyclic behaviour

Uses Software

• Kronos
• HyTech
• Uppaal

Cites Work

• Unnamed Item
• A theory of timed automata
• Lectures on Concurrency and Petri Nets
• Formal Modeling and Analysis of Timed Systems

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