Model Checking of RegCTL

Authors

  • Tomáš Brázdil
  • Ivana Černá

Keywords:

Finite state system, regular expression, tree automaton, temporal logic, model checking

Abstract

The paper is devoted to the problem of extending the temporal logic CTL so that it is more expressive and complicated properties can be expressed in a more readable form. The specification language RegCTL, an extension of CTL, is proposed. In RegCTL every CTL temporal operator is augmented with a regular expression, thus restricting moments when the validity is required. We propose a local distributed model checking algorithm for RegCTL.

Downloads

Download data is not yet available.

Downloads

Published

2012-01-30

How to Cite

Brázdil, T., & Černá, I. (2012). Model Checking of RegCTL. Computing and Informatics, 25(1), 81–97. Retrieved from http://147.213.75.17/ojs/index.php/cai/article/view/334

Most read articles by the same author(s)