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

No

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.
Displayed: 4/5/2026 20:09