Logics and translations for hierarchical model checking | Zendy

Norihiro Kamide | Zendy; Ryu Yano | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Logics and translations for hierarchical model checking

Author(s) -

Norihiro Kamide,

Ryu Yano

Publication year - 2017

Publication title -

procedia computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.334

H-Index - 76

ISSN - 1877-0509

DOI - 10.1016/j.procs.2017.08.014

Subject(s) - computation tree logic , ctl* , computer science , model checking , linear temporal logic , temporal logic , embedding , theoretical computer science , computation , hierarchical database model , algorithm , artificial intelligence , data mining , biochemistry , chemistry , cytotoxic t cell , in vitro

In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL) and computation-tree logic (CTL). Hierarchical model checking is a model checking paradigm that can appropriately verify systems with hierarchical information and structures. A sequential linear-time temporal logic (sLTL) and a sequential computation-tree logic (sCTL), which can suitably represent hierarchical information and structures, are developed by extending LTL and CTL, respectively. Translations from sLTL and sCTL into LTL and CTL, respectively, are defined, and theorems for embedding sLTL and sCTL into LTL and CTL, respectively, are proved using these translations. These embedding theorems allow us to reuse the standard LTL- and CTL-based model checking algorithms to verify hierarchical systems that are modeled and specified by sLTL and sCTL.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research