Propositional temporal logic is not suitable for expressing properties on the evolution of dynamically allocated entities over time. In particular, it is not possible to trace such...
In regular inference, the problem is to infer a regular language, typically represented by a deterministic finite automaton (DFA) from answers to a finite set of membership querie...
Abstract. We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be par...
Working in the context of a process-algebraic language for Probabilistic I/O Automata (PIOA), we study the notion of PIOA behavior equivalence by obtaining a complete axiomatizatio...
Eugene W. Stark, Rance Cleaveland, Scott A. Smolka
We give a brief overview of operational models for concurrent systems that exhibit probabilistic behavior, focussing on the interplay between probability and nondeterminism. Our su...
We propose a remedy to that part of the state-explosion problem for timed automata which is due to interleaving of actions. We prove the following quite surprising result: the unio...
Abstract We study the use of the elaboration preorder (due to ArunKumar and Natarajan) in the framework of up-to techniques for weak bisimulation. We show that elaboration yields a...
Timed concurrent systems are widely used in concurrent and distributed real-time software, modeling of hybrid systems, design of hardware systems (using hardware description langua...
Xiaojun Liu, Eleftherios Matsikoudis, Edward A. Le...
We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method s a system into a set of simple control flow cy...