Bounded Model Checking of Dense-Timed Deontic Interpreted Systems: A Satisfiability Modulo Theories Approach
Automated verification through the analysis of system models is often recommended to evaluate the correctness of safety-critical systems. Failures in such systems can have serious effects on both individuals and hardware. Historically, many automated verification techniques, including model checking...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2025-02-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/15/5/2487 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | Automated verification through the analysis of system models is often recommended to evaluate the correctness of safety-critical systems. Failures in such systems can have serious effects on both individuals and hardware. Historically, many automated verification techniques, including model checking, have been proposed and used to ensure the reliable development of real-time multi-agent systems (RTMASs). This paper investigates the use of Satisfiability Modulo Theories-based bounded model checking (SMT-based BMC) for the existential fragment of deontic epistemic metric temporal logic (EMTLKD), interpreted on models generated by dense-timed deontic interpreted systems (DTDISs). Specifically, we address the translation of the existential model checking problem for EMTLKD into the existential model checking problem for a variant of a deontic epistemic linear temporal logic (<inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msub><mi>ELTLKD</mi><mi mathvariant="normal">q</mi></msub></semantics></math></inline-formula>). Additionally, we present an SMT-based BMC approach tailored for <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><msub><mi>ELTLKD</mi><mi mathvariant="normal">q</mi></msub></semantics></math></inline-formula> and illustrate its effectiveness using a faulty train controller system as a representative example. Our approach is particularly applicable to engineering domains requiring high-assurance verification, such as railway control, autonomous vehicle coordination, and industrial automation. By formally verifying both timing and compliance constraints, our method supports engineers and system designers in developing more reliable and certifiable safety-critical systems before deployment. |
|---|---|
| ISSN: | 2076-3417 |