Unbounded, fully symbolic model checking of timed automata using Boolean methods.

DOI10.1007/B11831MaRDI QIDQ5900676zbMATH OpenOpenAlexFDO

Authors Sanjit A. Seshia, Randal E. Bryant

Publication date 20 April 2010

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

Full work available at URL https://doi.org/10.1007/b11831

Mathematics Subject Classification ID

Quantifier elimination, model completeness, and related topics (03C10) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1973987
• Bounded model checking for timed automata
• SAT-based unbounded model checking of timed automata
• Verification of timed automata via satisfiability checking
• Towards Bounded Model Checking for the Universal Fragment of TCTL

Cited in

(5)

• scientific article; zbMATH DE number 1973987 (Why is no real title available?)
• scientific article; zbMATH DE number 791802 (Why is no real title available?)
• SAT-based unbounded model checking of timed automata
• Timed automata verification and synthesis via finite automata learning
• Timed automata verification and synthesis via finite automata learning

Describes a project that uses

Uses Software

• Kronos
• Rabbit

This page was built for publication: Unbounded, fully symbolic model checking of timed automata using Boolean methods.

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