Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures

Warning

This publication doesn't include Faculty of Medicine. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2025
Type Article in Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
web https://atva-conference.org/2024/call-for-papers/accepted-papers/
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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info