Checking EMTLK properties of timed interpreted systems via bounded model checking

DOI10.1007/s11225-015-9637-9zbMath1417.68106OpenAlexW2219669608WikidataQ59471957 ScholiaQ59471957MaRDI QIDQ310082

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

Publication date: 7 September 2016

Published in: Studia Logica (Search for Journal in Brave)

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

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

Uses Software

• PicoSAT
• MCMAS
• MCK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Real-time logics: Complexity and expressiveness
• Bounded model checking for knowledge and real time
• Deontic interpreted systems
• The benefits of relaxing punctuality
• A New Translation from ECTL* to SAT
• A Translation of the Existential Model Checking Problem from MITL to HLTL
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Linear Encodings of Bounded LTL Model Checking
• Computer Aided Verification
• Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
• Bounded model checking using satisfiability solving

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