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.

Basic information

Original name

Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures

Authors

BENEŠ, Nikola; Luboš BRIM; Ondřej HUVAR; Samuel PASTVA and David ŠAFRÁNEK

Edition

Cham, International Symposium on Automated Technology for Verification and Analysis, ATVA 2024, p. 212-233, 22 pp. 2025

Publisher

Springer Nature Switzerland

Other information

Language

English

Type of outcome

Proceedings paper

Country of publisher

Switzerland

Confidentiality degree

is not subject to a state or trade secret

Publication form

electronic version available online

References:

URL

Marked to be transferred to RIV

Organization

Fakulta informatiky – Repository – Repository

ISBN

978-3-031-78750-8

ISSN

DOI

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

Keywords in English

Hybrid CTL; Model checking; Binary decision diagram; Coloured Kripke structures; Boolean networks

Links

MUNI/A/1592/2023, interní kód Repo.

Changed: 6/2/2026 00:50, RNDr. Daniel Jakubík

Abstract

In the original language

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.

Files attached

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

Cite

BENEŠ, Nikola; Luboš BRIM; Ondřej HUVAR; Samuel PASTVA and 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, p. 212-233. ISBN 978-3-031-78750-8. Available from: 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 and 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, p.~212-233. ISBN~978-3-031-78750-8. Available from: https://doi.org/10.1007/978-3-031-78750-8.

Přehled o publikaci