Issue No. 02 - April (1990 vol. 1)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/71.80145
<p>Real-time distributed systems are modeled by a times transition model (TTM). For any finite-state TTM, decision procedures are provided for checking a small but important class of properties (specified in real-time temporal logic). The procedures are linear in the size of the system reachability graph. The class of properties includes invariance, precedence, eventuality and real-time response specifications.</p>
Index Termspetri nets; parallel program design; timed transition models; finite-state TTM; decision procedures; real-time temporal logic; system reachability graph; invariance; precedence; eventuality; real-time response specifications; decidability; formal logic; formal specification; parallel programming; programming theory; real-time systems
J. Ostroff, "Deciding Properties of Timed Transition Models," in IEEE Transactions on Parallel & Distributed Systems, vol. 1, no. , pp. 170-183, 1990.