SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties

DOI10.16926/M.2015.20.08MaRDI QIDQ5040685zbMATH OpenOpenAlexFDO

Authors Bożena Woźna-Szcześniak, Ireneusz Szcześniak

Publication date 17 October 2022

Published in Scientific Issues Jan Długosz University in Częstochowa. Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.16926/m.2015.20.08

Mathematics Subject Classification ID

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

Recommendations

• Checking EMTLK properties of timed interpreted systems via bounded model checking
• Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata
• Simple SMT-based bounded model checking for timed interpreted systems
• Towards Bounded Model Checking for the Universal Fragment of TCTL
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking

Cited in

(8)

• SAT-based bounded model checking for weighted deontic interpreted systems
• Checking EMTLK properties of timed interpreted systems via bounded model checking
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking
• A comparison of SMT-solvers for timed weighted interpreted systems
• Comparing SAT- and SMT- based bounded model checking for ECTL properties
• Simple SMT-based bounded model checking for timed interpreted systems
• Verifying RTECTL properties of a train controller systems
• Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata

This page was built for publication: SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties

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