Checking EMTLK properties of timed interpreted systems via bounded model checking

DOI10.1007/S11225-015-9637-9MaRDI QIDQ310082zbMATH OpenOpenAlexWikidataFDO

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

Publication date 7 September 2016

Published in Studia Logica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s11225-015-9637-9

zbMATH Keywords

bounded model checkingmetric temporal logic with knowledgetimed interpreted systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70)

Recommendations

• SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
• Simple SMT-based bounded model checking for timed interpreted systems
• 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
• Towards Bounded Model Checking for the Universal Fragment of TCTL

Cites work

• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2064229 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• A new translation from ECTL* to SAT*
• A translation of the existential model checking problem from MITL to HLTL
• Bounded model checking for knowledge and real time
• Bounded model checking using satisfiability solving
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Computer Aided Verification
• Deontic interpreted systems
• Linear Encodings of Bounded LTL Model Checking
• Modal logic
• Real-time logics: Complexity and expressiveness
• The benefits of relaxing punctuality
• The complexity of epistemic model checking: clock semantics and branching time
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers

Cited in

(5)

• SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
• Simple SMT-based bounded model checking for timed interpreted systems
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• A comparison of SMT-solvers for timed weighted interpreted systems
• Comparing SAT- and SMT- based bounded model checking for ECTL properties

Describes a project that uses

Uses Software

• MCK
• MCMAS
• PicoSAT

This page was built for publication: Checking EMTLK properties of timed interpreted systems via bounded model checking

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