Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
| Authors | |
|---|---|
| Year of publication | 2025 |
| Type | Article in Proceedings |
| MU Faculty or unit | |
| Citation | |
| web | https://atva-conference.org/2024/call-for-papers/accepted-papers/ |
| Description | Hybrid CTL (HCTL) extends the branching-time temporal logic CTL with hybrid operators that refer to states, thus mixing first-order and modal logic features. The extended expressiveness of HCTL allows for the specification of properties that play a crucial role in analysing various dynamical systems describing complex physical or biological processes. Often, not all interactions in such processes are precisely known. An appropriate semantic structure is a collection of Kripke structures called a coloured Kripke structure. The paper proposes an entirely symbolic BDD-based algorithm for model checking HCTL on coloured Kripke structures. We discuss the correctness and complexity of the algorithm and consider some optimisations of the algorithm reflecting the structure of hybrid formulas. Finally, we evaluate the algorithm on several real-world cases. |
| Related projects: |