Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F25%3A00140613" target="_blank" >RIV/00216224:14330/25:00140613 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/chapter/10.1007/978-3-031-78750-8_11#chapter-info" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-78750-8_11#chapter-info</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-78750-8_11" target="_blank" >10.1007/978-3-031-78750-8_11</a>
Alternative languages
Result language
angličtina
Original language name
Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
Original language 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
S - Specificky vyzkum na vysokych skolach
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
International Symposium on Automated Technology for Verification and Analysis, ATVA 2024
ISBN
9783031787492
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
22
Pages from-to
212-233
Publisher name
Springer Nature Switzerland
Place of publication
Cham
Event location
Kyoto
Event date
Jan 1, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001456088200011