Title :
Deciding properties of timed transition models
Author :
Ostroff, Jonathan S.
Author_Institution :
Dept. of Comput. Sci., York Univ., Ont., Canada
fDate :
4/1/1990 12:00:00 AM
Abstract :
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
Keywords :
decidability; formal logic; formal specification; parallel programming; programming theory; real-time systems; decision procedures; eventuality; finite-state TTM; invariance; parallel program design; petri nets; precedence; real-time response specifications; real-time temporal logic; system reachability graph; timed transition models; Aerospace electronics; Clocks; Computational modeling; Concurrent computing; Heart; Logic; Performance analysis; Real time systems; Safety; Time to market;
Journal_Title :
Parallel and Distributed Systems, IEEE Transactions on
