The Power of Proofs: New Algorithms for Timed Automata Model Checking

DOI10.1007/978-3-319-10512-3_9MaRDI QIDQ5500559zbMATH OpenOpenAlexFDO

Authors Peter Fontana, Rance Cleaveland

Publication date 6 August 2015

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

Full work available at URL https://arxiv.org/abs/1408.6104

Mathematics Subject Classification ID

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

Abstract: This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L_{u,mu}^{mathitrel,mathitaf}$, and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an "on-the-fly" strategy based on proof search as a means of ensuring high performance for both positive and negative answers to model-checking questions. In particular, a set of proof rules for solving model-checking problems are given and proved sound and complete; we encode our algorithm in these proof rules and model-check a property by constructing a proof (or showing none exists) using these rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with emph{derived rules}, whose correctness can be inferred from the more primitive rules on which they are based. In this paper, we give the basic proof rules underlying our method, describe derived proof rules to improve performance, and compare our implementation of this model checker to the UPPAAL tool.

Recommendations

• The power of reachability testing for timed automata
• Publication:4508304
• Verified model checking of timed automata
• CONCUR 2005 – Concurrency Theory
• Verification of timed automata via satisfiability checking
• A proof-based method for modelling timed systems
• On improving backwards verification of timed automata (extended abstract)
• Robust Model-Checking of Linear-Time Properties in Timed Automata
• Improvements for the Symbolic Verification of Timed Automata
• scientific article; zbMATH DE number 1744956

Cited in

(4)

• The efficiency of identifying timed automata and the power of clocks
• A proof-based method for modelling timed systems
• Proving sequential function chart programs using timed automata
• scientific article; zbMATH DE number 1405651 (Why is no real title available?)

Describes a project that uses

Uses Software

• REDLIB
• Synthia
• CMC
• Uppaal
• Kronos

This page was built for publication: The Power of Proofs: New Algorithms for Timed Automata Model Checking

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