We study the model-checking problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal dependencies. The logic, which represents the logical counterpart of history-preserving bisimilarity, is ...

In game semantics, a computation is represented by a play, which is traditionally a sequence of messages exchanged by a program and an environment. Because of the sequentiality of plays, most game models for concurrent programs are a kind of ...

Model-based testing has mainly focused on models where concurrency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order ...

A method for data refinement over intervals is developed, together with a sound forward simulation rule.The framework enables reasoning about true concurrency between parallel processes.Methods for decomposing forward simulation proofs are developed.The ...

We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history-preserving bisimilarity, and fragments of the logic can be identified ...

Action systems have been shown to be applicable for modelling and constructing systems in both discrete and hybrid domains. We present a novel semantics for action systems using a sampling logic that facilitates reasoning about the truly concurrent ...

Scalability of cache coherence protocol is a key component in future shared-memory multi-core or multi-processor systems. The state space explosion is the first hurdle while applying model-checking to scalable protocols. In order to validate ...

Action refinement is an important operation in the hierarchical synthesis of concurrent systems. We propose an action refinement operator for E-LOTOS, a standard process-algebraic language for formal specification of real-time, concurrent and reactive ...

E-LOTOS is a standard process-algebraic language for formal specification of real-time concurrent and reactive systems. Its originally defined semantics is based on interleaving of events. In the present paper, we propose an enhanced kind of event ...

In modular approaches to specify concurrent systems a system is built up from components using various operators as e.g. the sequential, the parallel, or the choice (+) operator. Usually the choice between two components, i.e. P₁ + P₂, is taken in ...

Designers of network algorithms often give elegant informal descriptions of the intuition behind their algorithms (see [GHS83, Hum83, MeS79, Seg82, Seg83, ZeS80]). Usually these descriptions are structured as if subtasks are performed one after ...

This paper argues that partial order semantics can be used profitably in the proofs of some nontrivial results in Petri net theory. We show that most of Commoner's and Hack's structure theory of free choice nets can be phrased and proved in terms ...

We present a variety of denotational linear time semantics for a language with recursion and "true" concurrency in a form of synchronous co-operation, which in the literature is known as step semantics. We show that this can be done by a generalization ...