Symbolic Model Checking of Hybrid CTL on Coloured Kripke
Structures

Přehled o publikaci

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

Jazyk

angličtina

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"

Odkazy

URL

Označené pro přenos do RIV

Organizace

Fakulta informatiky – Masarykova univerzita – Repozitář

ISBN

978-3-031-78750-8

ISSN

DOI

https://doi.org/10.1007/978-3-031-78750-8

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.

Změněno: 6. 2. 2026 00:50, RNDr. Daniel Jakubík

Anotace

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.

Přiložené soubory

https://is.muni.cz/publication/2475011/atva2024.pdf

Citovat

BENEŠ, Nikola; Luboš BRIM; Ondřej HUVAR; Samuel PASTVA a David ŠAFRÁNEK. Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures. Online. In International Symposium on Automated Technology for Verification and Analysis, ATVA 2024. Cham: Springer Nature Switzerland, 2025, s. 212-233. ISBN 978-3-031-78750-8. Dostupné z: https://doi.org/10.1007/978-3-031-78750-8.

@inproceedings{89366,
   author = {Beneš, Nikola and Brim, Luboš and Huvar, Ondřej and Pastva, Samuel and Šafránek, David},
   address = {Cham},
   booktitle = {International Symposium on Automated Technology for Verification and Analysis, ATVA 2024},
   doi = {https://doi.org/10.1007/978-3-031-78750-8},
   keywords = {Hybrid CTL; Model checking; Binary decision diagram; Coloured Kripke structures; Boolean networks},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-78750-8},
   pages = {212-233},
   publisher = {Springer Nature Switzerland},
   title = {Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-78750-8_11#chapter-info},
   year = {2025}
}

TY  - CONF
ID  - 89366
AU  - Beneš, Nikola - Brim, Luboš - Huvar, Ondřej - Pastva, Samuel - Šafránek, David
PY  - 2025
TI  - Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
PB  - Springer Nature Switzerland
CY  - Cham
SN  - 9783031787508
KW  - Hybrid CTL
KW  - Model checking
KW  - Binary decision diagram
KW  - Coloured Kripke structures
KW  - Boolean networks
UR  - https://link.springer.com/chapter/10.1007/978-3-031-78750-8_11#chapter-info
N2  - 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.
ER  -

BENEŠ, Nikola; Luboš BRIM; Ondřej HUVAR; Samuel PASTVA a David ŠAFRÁNEK. Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures. Online. In \textit{International Symposium on Automated Technology for Verification and Analysis, ATVA 2024}. Cham: Springer Nature Switzerland, 2025, s.~212-233. ISBN~978-3-031-78750-8. Dostupné z: https://doi.org/10.1007/978-3-031-78750-8.

Přehled o publikaci