Journal of the Japanese Society for Artificial Intelligence
Online ISSN : 2435-8614
Print ISSN : 2188-2266
Print ISSN:0912-8085 until 2013
The Extension of Real-Time Temporal Logic and the Method of Model-Checking Verification
Satoshi YAMANE
Author information
MAGAZINE FREE ACCESS

1997 Volume 12 Issue 3 Pages 448-455

Details
Abstract

Real-time systems consist of many concurrent processes and behave on strict timing conditions. It is important to verify the timing conditions of real-time systems. In this paper, we propose extended real-time temporal logic and effective real-time model checking as follows. (1) The timing description of extended real-time temporal logic consists of both freeze quantification and branching time structure in dense time model. For this extension, extended real-time temporal logic admits timing constraints between distant contexts. (2) System specification is described by parallel composition of timed automata. Timed Kripke structure is automatically generated from timed automaton. (3) Real time model checking consists of both labelling algorithm and geometric region. This method is shown effective by some example.

Content from these authors
© 1997 The Japaense Society for Artificial Intelligence
Previous article Next article
feedback
Top