Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFull abstraction for fair testing in CCS
259
0
0.0
(
0
)
Added by
Tom Hirschowitz
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Authors
Tom Hirschowitz
Ask ChatGPT about the research
No Arabic abstract
In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent presheaf semantics and as a concurrent game semantics. It is here proved that a behavioural equivalence induced by this semantics on CCS processes is fully abstract for fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the rule of the game. From any playground, two languages, equipped with labelled transition systems, are derived, as well as a strong, functional bisimulation between them.
rate research
Read More
In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent form of presheaf semantics and as a concurrent form of game semantics. We define in this setting an analogue of fair testing equivalence, which we prove fully abstract w.r.t. standard fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the `rule of the game. From any playground, we derive two languages equipped with labelled transition systems, as well as a strong, functional bisimulation between them.
We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if the language is globally call-by-name, we allow a call-by-value evaluation for ground type arguments in order to provide the language with a suitable algorithmic expressiveness. We describe a denotational semantics based on probabilistic coherence spaces, a model of classical Linear Logic developed in previous works. We prove an adequacy and an equational full abstraction theorem showing that equality in the model coincides with a natural notion of observational equivalence.
Partially Observable Markov Decision Process (POMDP) is widely used to model probabilistic behavior for complex systems. Compared with MDPs, POMDP models a system more accurate but solving a POMDP generally takes exponential time in the size of its state space. This makes the formal verification and synthesis problems much more challenging for POMDPs, especially when multiple system components are involved. As a promising technique to reduce the verification complexity, the abstraction method tries to find an abstract system with a smaller state space but preserves enough properties for the verification purpose. While abstraction based verification has been explored extensively for MDPs, in this paper, we present the first result of POMDP abstraction and its refinement techniques. The main idea follows the counterexample-guided abstraction refinement (CEGAR) framework. Starting with a coarse guess for the POMDP abstraction, we iteratively use counterexamples from formal verification to refine the abstraction until the abstract system can be used to infer the verification result for the original POMDP. Our main contributions have two folds: 1) we propose a novel abstract system model for POMDP and a new simulation relation to capture the partial observability then prove the preservation on a fragment of Probabilistic Computation Tree Logic (PCTL); 2) to find a proper abstract system that can prove or disprove the satisfaction relation on the concrete POMDP, we develop a novel refinement algorithm. Our work leads to a sound and complete CEGAR framework for POMDP.
In this paper, we extend the theory CCS for trees (CCTS) to value-passing CCTS (VCCTS), of which symbols have the capacity for receiving and sending data values, and a nonsequential semantics is proposed in an operational approach. In this concurrent model, a weak barbed congruence and a localized early weak bisimilarity are defined, and the latter relation is proved to be sufficient to justify the former. As an illustration of potential applications of VCCTS, a semantics based on VCCTS is given to a toy multi-threaded programming language featuring a core of C/C++ concurrency; and a formalization based on the operational semantics of VCCTS is proposed for some relaxed memory models, and a DRF-guarantee property with respect to VCCTS is proved.
This paper provides a fully abstract semantics for value-passing CCS for trees (VCCTS). The operational semantics is given both in terms of a reduction semantics and in terms of a labelled transition semantics. The labelled transition semantics is non-sequential, allowing more than one action occurring simultaneously. We develop the theory of behavioral equivalence by introducing both weak barbed congruence and weak bisimilarity. In particular, we show that weak barbed congruence coincides with weak bisimilarity on image-finite processes. This is the first such result for a concurrent model with tree structures. Distributed systems can be naturally modeled by means of this graph-based system, and some examples are given to illustrate this.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
