D
2025
Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
BENEŠ, Nikola; Luboš BRIM; Ondřej HUVAR; Samuel PASTVA; David ŠAFRÁNEK et al.
Základní údaje
Originální název
Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
Autoři
BENEŠ, Nikola; Luboš BRIM; Ondřej HUVAR; Samuel PASTVA a David ŠAFRÁNEK
Vydání
Cham, International Symposium on Automated Technology for Verification and Analysis, ATVA 2024, od s. 212-233, 22 s. 2025
Nakladatel
Springer Nature Switzerland
Další údaje
Typ výsledku
Stať ve sborníku
Stát vydavatele
Švýcarsko
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
elektronická verze "online"
Označené pro přenos do RIV
Ne
Organizace
Fakulta informatiky – Masarykova univerzita – Repozitář
Klíčová slova anglicky
Hybrid CTL; Model checking; Binary decision diagram; Coloured Kripke structures; Boolean networks
Návaznosti
MUNI/A/1592/2023, interní kód Repo.
V originále
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.
Zobrazeno: 4. 5. 2026 19:09