This paper presents a new formalism and a new algorithm for verifying timed circuits. The formalism, called orbital nets, allows hierarchical verification based on abehavioralseman...
Relational Coarsest Partition Problems (RCPPs) play a vital role in verifying concurrent systems. It is known that RCPPs are P-complete and hence it may not be possible to design ...
We introduce event-recording automata. An event-recording automaton is a timed automaton that contains, for every event a, a clock that records the time of the last occurrence of a...