Automatically assigned DDC number: 00433

Manually assigned DDC number: 00433

Number of references: 0

Title: Model-Checking in Dense Real-time

Author:

Author:

Author:

Subject: Rajeev Alur,Costas Courcoubetis,David Dill Model-Checking in Dense Real-time

Description: . Model-checking is a method of verifying concurrent systems in which a state-transition graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking for the branching-time logic CTL to the analysis of real-time systems, whose correctness depends on the magnitudes of the timing delays. For specifications, we extend the syntax of CTL to allow quantitative temporal operators such as 93!5 , meaning "possibly within 5 time units." The formulas of the resulting logic, Timed CTL (TCTL), are interpreted over continuous computation trees, trees in which paths are maps from the set of nonnegative reals to system states. To model finitestate systems we introduce timed graphs --- state-transition graphs annotated with timing constraints. As our main result, we develop an algorithm for model-checking, for determining the truth of a TCTL-formula with respect to a timed graph. We argue that choosing a dense domain instead of a discrete domain to mo...

Contributor: The Pennsylvania State University CiteSeer Archives

Publisher: unknown

Date: 1997-10-22

Pubyear: 1993

Format: ps

Identifier: http://citeseer.ist.psu.edu/140487.html

Source: http://www.cs.ubc.ca/spider/ajh/courses/cpsc513/ACD93.ps

Language: en

Rights: unrestricted

Graph

<?xml   version="1.0"   encoding="UTF-8"?>

<references_metadata>

      <rec   ID="SELF"   Type="SELF"   CiteSeer_Book="SELF"   CiteSeer_Volume="SELF"   Title="Model-Checking   in   Dense   Real-time">

            <identifier   Org="ISBN:0471184063"   Paper_ID="SELF"   Extracted="0471184063"   DDC="658.4038"   Normalized_DDC="6584038"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:0769503063"   Paper_ID="SELF"   Extracted="0769503063"   />

            <identifier   Org="ISBN:354022940X"   Paper_ID="SELF"   Extracted="354022940X"   DDC="004.35"   Normalized_DDC="00435"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540253882"   Paper_ID="SELF"   Extracted="3540253882"   DDC="004"   Normalized_DDC="004"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:354028060X"   Paper_ID="SELF"   Extracted="354028060X"   DDC="004.01/5113"   Normalized_DDC="004015113"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540405615"   Paper_ID="SELF"   Extracted="3540405615"   DDC="004"   Normalized_DDC="004"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540434194"   Paper_ID="SELF"   Extracted="3540434194"   DDC="004.2/1"   Normalized_DDC="00421"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540436316"   Paper_ID="SELF"   Extracted="3540436316"   DDC="005.1/4"   Normalized_DDC="00514"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540441654"   Paper_ID="SELF"   Extracted="3540441654"   DDC="004/.33"   Normalized_DDC="00433"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:354062600X"   Paper_ID="SELF"   Extracted="354062600X"   DDC="004.1/9"   Normalized_DDC="00419"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540650032"   Paper_ID="SELF"   Extracted="3540650032"   DDC="004/.33"   Normalized_DDC="00433"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540660100"   Paper_ID="SELF"   Extracted="3540660100"   />

            <identifier   Org="ISBN:3540662022"   Paper_ID="SELF"   Extracted="3540662022"   DDC="004.24"   Normalized_DDC="00424"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540664084"   Paper_ID="SELF"   Extracted="3540664084"   DDC="001.64"   Normalized_DDC="00164"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540678972"   Paper_ID="SELF"   Extracted="3540678972"   DDC="001.64"   Normalized_DDC="00164"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540698493"   Paper_ID="SELF"   Extracted="3540698493"   />

            <identifier   Org="ISBN:3540712089"   Paper_ID="SELF"   Extracted="3540712089"   />

            <identifier   Org="ISBN:354073550X"   Paper_ID="SELF"   Extracted="354073550X"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.06666666666666667"   />

            <identifier   Org="ISBN:3540766480"   Paper_ID="SELF"   Extracted="3540766480"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.06666666666666667"   />

      </rec>

</references_metadata>