Search
Now showing items 1-7 of 7
Forward and Backward Simulations Part I: Untimed Systems (Replaces TM-486)
(1993-03)
A unified, comprehensive presentation of simulation techniques for verification of concurrent systems is given, in terms of a simple untimed automaton model. In particular, (1) refinements, (2) forward and backward ...
Compositionality for Probabilistic Automata
We establish that on the dfomain of probabilistic automata, the trace distribution preorder coincides with the simulation preorder.
Hybrid I/O Automata*
(2003-01)
Hybrid systems are systems that exhibit a combination of discrete and continuous behavior. Typical hybrid systems include computer components, which operate in discrete program steps, and real-world components, whose ...
Forward and Backward Simulations for Timing-based Systems
(1991-11)
A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. As a first step, a comprehensive overview of simulation ...
Forward and Backward Simulations Part II: Timing-based Systems
(1993-03)
A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. These techniques include (1) refinments, (2) forward and ...
Hybrid I/O Automata
(1995-12)
We propose a new hybrid I/O automaton model that is capable of describing both continuous and discrete behavior. The model, which extends the timed I/O automaton model of [12, 7] and the phase transition system models of ...
Action Transducers and Timed Automata
(1992-11)
The timed automaton model of [29, 30] is a general model for timing-based systems. A notion of timed action transducer is here defined as an automata-theoretic way of representing operations on timed automata. It is shown ...