Simple SMT-based bounded model checking for timed interpreted systems

DOI10.1007/978-3-319-60840-2_35MaRDI QIDQ5082182zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Agnieszka M. Zbrzezny, Andrzej Zbrzezny

Publication date 15 June 2022

Published in Rough Sets (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-60840-2_35

Mathematics Subject Classification ID

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

Recommendations

• Checking EMTLK properties of timed interpreted systems via bounded model checking
• SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking

Cited in

(6)

• SMT-based induction methods for timed systems
• SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking
• Checking EMTLK properties of timed interpreted systems via bounded model checking
• SMT-based reachability analysis for simply-timed systems
• A comparison of SMT-solvers for timed weighted interpreted systems

This page was built for publication: Simple SMT-based bounded model checking for timed interpreted systems

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