Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2025

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

International Symposium on Automated Technology for Verification and Analysis, ATVA 2024

ISBN

9783031787492

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

22

Strana od-do

212-233

Název nakladatele

Springer Nature Switzerland

Místo vydání

Cham

Místo konání akce

Kyoto

Datum konání akce

1. 1. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001456088200011