Volume 11, Issue 2

2015


1. Mutually Testing Processes

Bernardi, Giovanni ; Hennessy, Matthew.
In the standard testing theory of DeNicola-Hennessy one process is considered to be a refinement of another if every test guaranteed by the former is also guaranteed by the latter. In the domain of web services this has been recast, with processes viewed as servers and tests as clients. In this way […]

2. On Reachability for Unidirectional Channel Systems Extended with Regular Tests

Petr, Jancar ; Karandikar, Prateek ; Schnoebelen, Philippe.
"Unidirectional channel systems" (Chambart & Schnoebelen, CONCUR 2008) are finite-state systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equipping them […]

3. Learning and Designing Stochastic Processes from Logical Constraints

Bortolussi, Luca ; Sanguinetti, Guido.
Stochastic processes offer a flexible mathematical formalism to model and reason about systems. Most analysis tools, however, start from the premises that models are fully specified, so that any parameters controlling the system's dynamics must be known exactly. As this is seldom the case, […]

4. Containment for Conditional Tree Patterns

Facchini, Alessandro ; Hirai, Yoichi ; Marx, Maarten ; Sherkhonov, Evgeny.
A Conditional Tree Pattern (CTP) expands an XML tree pattern with labels attached to the descendant edges. These labels can be XML element names or Boolean CTPs. The meaning of a descendant edge labelled by A and ending in a node labelled by B is a path of child steps ending in a B node such that […]

5. From Kleisli Categories to Commutative C*-algebras: Probabilistic Gelfand Duality

Furber, Robert W. J. ; Jacobs, Bart P. F..
C*-algebras form rather general and rich mathematical structures that can be studied with different morphisms (preserving multiplication, or not), and with different properties (commutative, or not). These various options can be used to incorporate various styles of computation (set-theoretic, […]

6. Bounding linear head reduction and visible interaction through skeletons

Clairambault, Pierre.
In this paper, we study the complexity of execution in higher-order programming languages. Our study has two facets: on the one hand we give an upper bound to the length of interactions between bounded P-visible strategies in Hyland-Ong game semantics. This result covers models of […]

7. Using models to model-check recursive schemes

Salvati, Sylvain ; Walukiewicz, Igor.
We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose the use of a model of lambda-Y-calculus to discriminate the terms that satisfy a given […]

8. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic

Pich, Ján.
We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV1 (no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the (n,d,{\lambda})-graphs in […]

9. Pure Nash Equilibria in Concurrent Deterministic Games

Bouyer, Patricia ; Brenguier, Romain ; Markey, Nicolas ; Ummels, Michael.
We study pure-strategy Nash equilibria in multi-player concurrent deterministic games, for a variety of preference relations. We provide a novel construction, called the suspect game, which transforms a multi-player concurrent game into a two-player turn-based game which turns Nash equilibria into […]

10. Generators and relations for n-qubit Clifford operators

Selinger, Peter.
We define a normal form for Clifford circuits, and we prove that every Clifford operator has a unique normal form. Moreover, we present a rewrite system by which any Clifford circuit can be reduced to normal form. This yields a presentation of Clifford operators in terms of generators and […]

11. On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry

Marshall, Andrew M ; Meadows, Catherine ; Narendran, Paliath.
An algorithm for unification modulo one-sided distributivity is an early result by Tid\'en and Arnborg. More recently this theory has been of interest in cryptographic protocol analysis due to the fact that many cryptographic operators satisfy this property. Unfortunately the algorithm presented in […]

12. Deciding the value 1 problem for probabilistic leaktight automata

Fijalkow, Nathanaël ; Gimbert, Hugo ; Kelmendi, Edon ; Oualhadj, Youssouf.
The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1? This problem was proved undecidable recently; to overcome this, several classes of probabilistic automata […]

13. Thermodynamic graph-rewriting

Danos, Vincent ; Harmer, Russell ; Honorato-Zimmer, Ricardo.
We develop a new thermodynamic approach to stochastic graph-rewriting. The ingredients are a finite set of reversible graph-rewriting rules called generating rules, a finite set of connected graphs P called energy patterns and an energy cost function. The idea is that the generators define the […]

14. Weak bisimulation for coalgebras over order enriched monads

Brengos, Tomasz.
The paper introduces the notion of a weak bisimulation for coalgebras whose type is a monad satisfying some extra properties. In the first part of the paper we argue that systems with silent moves should be modelled coalgebraically as coalgebras whose type is a monad. We show that the visible and […]

15. On absorption in semigroups and $n$-ary semigroups

Bašić, Bojan.
The notion of absorption was developed a few years ago by Barto and Kozik and immediately found many applications, particularly in topics related to the constraint satisfaction problem. We investigate the behavior of absorption in semigroups and n-ary semigroups (that is, algebras with one n-ary […]

16. Permissive Controller Synthesis for Probabilistic Systems

Drager, Klaus ; Forejt, Vojtech ; Kwiatkowska, Marta ; Parker, David ; Ujma, Mateusz.
We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty […]