Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time

DOI10.1007/978-3-540-85762-4_20MaRDI QIDQ5505609zbMATH OpenOpenAlexFDO

Authors Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro

Publication date 27 January 2009

Published in Theoretical Aspects of Computing - ICTAC 2008 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85762-4_20

zbMATH Keywords

bi-infinite words and automatabounded model checkingmetric temporal logic

Mathematics Subject Classification ID

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

Recommendations

• Bounded model checking of infinite state systems
• Time-Bounded Verification
• Bounded model checking for timed automata
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
• Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata

Cites work

• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 1956570 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2206109 (Why is no real title available?)
• Langages algébriques de mots biinfinis. (Algebraic languages of biinfinite words)
• Linear Encodings of Bounded LTL Model Checking
• Theory and Applications of Satisfiability Testing
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Early verification of legal compliance via bounded satisfiability checking

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time

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