Showing 1–18 of 18 results for author: Lozes, E

Weakly synchronous systems with three machines are Turing powerful

Authors: Cinzia Di Giusto, Davide Ferré, Etienne Lozes, Nicolas Nisse

Abstract: Communicating finite-state machines (CFMs) are a Turing powerful model of asynchronous message-passing distributed systems. In weakly synchronous systems, processes communicate through phases in which messages are first sent and then received, for each process. Such systems enjoy a limited form of synchronization, and for some communication models, this restriction is enough to make the reachabili… ▽ More Communicating finite-state machines (CFMs) are a Turing powerful model of asynchronous message-passing distributed systems. In weakly synchronous systems, processes communicate through phases in which messages are first sent and then received, for each process. Such systems enjoy a limited form of synchronization, and for some communication models, this restriction is enough to make the reachability problem decidable. In particular, we explore the intriguing case of p2p (FIFO) communication, for which the reachability problem is known to be undecidable for four processes, but decidable for two. We show that the configuration reachability problem for weakly synchronous systems of three processes is undecidable. This result is heavily inspired by our study on the treewidth of the Message Sequence Charts (MSCs) that might be generated by such systems. In this sense, the main contribution of this work is a weakly synchronous system with three processes that generates MSCs of arbitrarily large treewidth. △ Less

Submitted 21 August, 2023; originally announced August 2023.

A partial order view of message-passing communication models

Authors: Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, Etienne Lozes

Abstract: There is a wide variety of message-passing communication models, ranging from synchronous ''rendez-vous'' communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the network, and a few classes of orders of message delivery (FIFO, causally ordered) have been identified in the early days of… ▽ More There is a wide variety of message-passing communication models, ranging from synchronous ''rendez-vous'' communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the network, and a few classes of orders of message delivery (FIFO, causally ordered) have been identified in the early days of distributed computing. For local-scale message-passing applications, e.g., running on a single machine, the communication model may be determined by the actual implementation of message buffers and by how FIFO queues are used. While large-scale communication models, such as causal ordering, are defined by logical axioms, local-scale models are often defined by an operational semantics. In this work, we connect these two approaches, and we present a unified hierarchy of communication models encompassing both large-scale and local-scale models, based on their concurrent behaviors. We also show that all the communication models we consider can be axiomatized in the monadic second order logic, and may therefore benefit from several bounded verification techniques based on bounded special treewidth. △ Less

Submitted 13 January, 2023; v1 submitted 24 October, 2022; originally announced October 2022.

Towards Generalised Half-Duplex Systems

Authors: Cinzia Di Giusto, Loïc Germerie Guizouarn, Etienne Lozes

Abstract: FIFO automata are finite state machines communicating through FIFO queues. They can be used for instance to model distributed protocols. Due to the unboundedness of the FIFO queues, several verification problems are undecidable for these systems. In order to model-check such systems, one may look for decidable subclasses of FIFO systems. Binary half-duplex systems are systems of two FIFO automata… ▽ More FIFO automata are finite state machines communicating through FIFO queues. They can be used for instance to model distributed protocols. Due to the unboundedness of the FIFO queues, several verification problems are undecidable for these systems. In order to model-check such systems, one may look for decidable subclasses of FIFO systems. Binary half-duplex systems are systems of two FIFO automata exchanging over a half-duplex channel. They were studied by Cece and Finkel who established the decidability in polynomial time of several properties. These authors also identified some problems in generalising half-duplex systems to multi-party communications. We introduce greedy systems, as a candidate to generalise binary half-duplex systems. We show that greedy systems retain the same good properties as binary half-duplex systems, and that, in the setting of mailbox communications, greedy systems are quite closely related to a multiparty generalisation of half-duplex systems. △ Less

Submitted 30 September, 2021; originally announced October 2021.

Comments: In Proceedings ICE 2021, arXiv:2109.14908

Journal ref: EPTCS 347, 2021, pp. 22-37

Guessing the buffer bound for k-synchronizability

Authors: Cinzia Di Giusto, Laetitia Laversa, Etienne Lozes

Abstract: A communicating system is $k$-synchronizable if all of the message sequence charts representing the executions can be divided into slices of $k$ sends followed by $k$ receptions. It was previously shown that, for a fixed given $k$, one could decide whether a communicating system is $k$-synchronizable. This result is interesting because the reachability problem can be solved for $k$-synchronizable… ▽ More A communicating system is $k$-synchronizable if all of the message sequence charts representing the executions can be divided into slices of $k$ sends followed by $k$ receptions. It was previously shown that, for a fixed given $k$, one could decide whether a communicating system is $k$-synchronizable. This result is interesting because the reachability problem can be solved for $k$-synchronizable systems. However, the decision procedure assumes that the bound $k$ is fixed. In this paper we improve this result and show that it is possible to decide if such a bound $k$ exists. △ Less

Submitted 29 April, 2021; originally announced April 2021.

Comments: Long version of CIAA paper (19 pages)

A Complete Axiomatisation for Quantifier-Free Separation Logic

Authors: Stéphane Demri, Étienne Lozes, Alessio Mansutti

Abstract: We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-sty… ▽ More We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: the axiomatisation of core formulae where Boolean combinations of core formulae capture the expressivity of the whole logic, axioms and inference rules to simulate a bottom-up elimination of separating connectives, and finally structural axioms and inference rules from propositional calculus and Boolean BI with the magic wand. △ Less

Submitted 9 August, 2021; v1 submitted 9 June, 2020; originally announced June 2020.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 3 (August 10, 2021) lmcs:6548

Internal Calculi for Separation Logics

Authors: Stéphane Demri, Etienne Lozes, Alessio Mansutti

Abstract: We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic. We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predic… ▽ More We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic. We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem. △ Less

Submitted 11 October, 2019; originally announced October 2019.

On the k-synchronizability of systems

Authors: Cinzia Di Giusto, Cinzia Giusto, Laetitia Laversa, Etienne Lozes

Abstract: In this paper, we work on the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem… ▽ More In this paper, we work on the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata. △ Less

Submitted 21 January, 2020; v1 submitted 4 September, 2019; originally announced September 2019.

The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic

Authors: Stéphane Demri, Etienne Lozes, Alessio Mansutti

Abstract: The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and veri… ▽ More The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic. △ Less

Submitted 28 February, 2021; v1 submitted 12 October, 2018; originally announced October 2018.

Synchronizability of Communicating Finite State Machines is not Decidable

Authors: Alain Finkel, Etienne Lozes

Abstract: A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thank… ▽ More A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set. △ Less

Submitted 19 December, 2023; v1 submitted 23 February, 2017; originally announced February 2017.

Comments: Long version

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 4 (December 20, 2023) lmcs:4764

Multi-Buffer Simulations for Trace Language Inclusion

Authors: Milka Hutagalung, Norbert Hundeshagen, Dietrich Kuske, Martin Lange, Etienne Lozes

Abstract: We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study… ▽ More We consider simulation games played between Spoiler and Duplicator on two Büchi automata in which the choices made by Spoiler can be buffered by Duplicator in several buffers before she executes them on her structure. We show that the simulation games are useful to approximate the inclusion of trace closures of languages accepted by finite-state automata, which is known to be undecidable. We study the decidability and complexity and show that the game with bounded buffers can be decided in polynomial time, whereas the game with one unbounded and one bounded buffer is highly undecidable. We also show some sufficient conditions on the automata for Duplicator to win the game (with unbounded buffers). △ Less

Submitted 13 September, 2016; originally announced September 2016.

Comments: In Proceedings GandALF 2016, arXiv:1609.03648

Journal ref: EPTCS 226, 2016, pp. 213-227

Two-Buffer Simulation Games

Authors: Milka Hutagalung, Norbert Hundeshagen, Dietrich Kuske, Martin Lange, Etienne Lozes

Abstract: We consider simulation games played between Spoiler and Duplicator on two Buchi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she executes them on her structure. Previous work on such games using a single buffer has shown that they are useful to approximate language inclusion problems. We study the decidability and complexity and show t… ▽ More We consider simulation games played between Spoiler and Duplicator on two Buchi automata in which the choices made by Spoiler can be buffered by Duplicator in two different buffers before she executes them on her structure. Previous work on such games using a single buffer has shown that they are useful to approximate language inclusion problems. We study the decidability and complexity and show that games with two buffers can be used to approximate corresponding problems on finite transducers, i.e. the inclusion problem for rational relations over infinite words. △ Less

Submitted 1 August, 2016; originally announced August 2016.

Comments: In Proceedings Cassting'16/SynCoP'16, arXiv:1608.00177

Journal ref: EPTCS 220, 2016, pp. 27-38

A Type-Directed Negation Elimination

Authors: Etienne Lozes

Abstract: In the modal mu-calculus, a formula is well-formed if each recursive variable occurs underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any well-formed formula into an equivalent formula without negations -- its negation normal form. Moreover, if the formula is of size n, its negation normal form of is of the same size O(n). The full modal mu-calculus a… ▽ More In the modal mu-calculus, a formula is well-formed if each recursive variable occurs underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any well-formed formula into an equivalent formula without negations -- its negation normal form. Moreover, if the formula is of size n, its negation normal form of is of the same size O(n). The full modal mu-calculus and the negation normal form fragment are thus equally expressive and concise. In this paper we extend this result to the higher-order modal fixed point logic (HFL), an extension of the modal mu-calculus with higher-order recursive predicate transformers. We present a procedure that converts a formula into an equivalent formula without negations of quadratic size in the worst case and of linear size when the number of variables of the formula is fixed. △ Less

Submitted 10 September, 2015; originally announced September 2015.

Comments: In Proceedings FICS 2015, arXiv:1509.02826

ACM Class: F4.1

Journal ref: EPTCS 191, 2015, pp. 132-142

Buffered Simulation Games for Büchi Automata

Authors: Milka Hutagalung, Martin Lange, Etienne Lozes

Abstract: Simulation relations are an important tool in automata theory because they provide efficiently computable approximations to language inclusion. In recent years, extensions of ordinary simulations have been studied, for instance multi-pebble and multi-letter simulations which yield better approximations and are still polynomial-time computable. In this paper we study the limitations of approxima… ▽ More Simulation relations are an important tool in automata theory because they provide efficiently computable approximations to language inclusion. In recent years, extensions of ordinary simulations have been studied, for instance multi-pebble and multi-letter simulations which yield better approximations and are still polynomial-time computable. In this paper we study the limitations of approximating language inclusion in this way: we introduce a natural extension of multi-letter simulations called buffered simulations. They are based on a simulation game in which the two players share a FIFO buffer of unbounded size. We consider two variants of these buffered games called continuous and look-ahead simulation which differ in how elements can be removed from the FIFO buffer. We show that look-ahead simulation, the simpler one, is already PSPACE-hard, i.e. computationally as hard as language inclusion itself. Continuous simulation is even EXPTIME-hard. We also provide matching upper bounds for solving these games with infinite state spaces. △ Less

Submitted 21 May, 2014; originally announced May 2014.

Comments: In Proceedings AFL 2014, arXiv:1405.5272

Journal ref: EPTCS 151, 2014, pp. 286-300

Shared Contract-Obedient Endpoints

Authors: Étienne Lozes, Jules Villard

Abstract: Most of the existing verification techniques for message-passing programs suppose either that channel endpoints are used in a linear fashion, where at most one thread may send or receive from an endpoint at any given time, or that endpoints may be used arbitrarily by any number of threads. The former approach usually forbids the sharing of channels while the latter limits what is provable about pr… ▽ More Most of the existing verification techniques for message-passing programs suppose either that channel endpoints are used in a linear fashion, where at most one thread may send or receive from an endpoint at any given time, or that endpoints may be used arbitrarily by any number of threads. The former approach usually forbids the sharing of channels while the latter limits what is provable about programs. In this paper we propose a midpoint between these techniques by extending a proof system based on separation logic to allow sharing of endpoints. We identify two independent mechanisms for supporting sharing: an extension of fractional shares to endpoints, and a new technique based on what we call reflexive ownership transfer. We demonstrate on a number of examples that a linear treatment of sharing is possible. △ Less

Submitted 16 December, 2012; originally announced December 2012.

Comments: In Proceedings ICE 2012, arXiv:1212.3458

ACM Class: F.3.1

Journal ref: EPTCS 104, 2012, pp. 17-31

Model-Checking Process Equivalences

Authors: Martin Lange, Etienne Lozes, Manuel Vargas Guzmán

Abstract: Process equivalences are formal methods that relate programs and system which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic systems to display the same behaviour there are a multitude of formal process equivalences, ranging from bisimulation to trace equivalence, categorised in the linear-time branching-time spectrum. We present a logical… ▽ More Process equivalences are formal methods that relate programs and system which, informally, behave in the same way. Since there is no unique notion of what it means for two dynamic systems to display the same behaviour there are a multitude of formal process equivalences, ranging from bisimulation to trace equivalence, categorised in the linear-time branching-time spectrum. We present a logical framework based on an expressive modal fixpoint logic which is capable of defining many process equivalence relations: for each such equivalence there is a fixed formula which is satisfied by a pair of processes if and only if they are equivalent with respect to this relation. We explain how to do model checking, even symbolically, for a significant fragment of this logic that captures many process equivalences. This allows model checking technology to be used for process equivalence checking. We show how partial evaluation can be used to obtain decision procedures for process equivalences from the generic model checking scheme. △ Less

Submitted 8 October, 2012; originally announced October 2012.

Comments: In Proceedings GandALF 2012, arXiv:1210.2028

ACM Class: F.4.1

Journal ref: EPTCS 96, 2012, pp. 43-56

Model-Checking the Higher-Dimensional Modal mu-Calculus

Authors: Martin Lange, Etienne Lozes

Abstract: The higher-dimensional modal mu-calculus is an extension of the mu-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property that can be expressed in this logic can be checked in polynomial time, and conversely every polynomial-time decidable problem that has a bisimulation-invariant encoding into labeled transition systems can also be defined in… ▽ More The higher-dimensional modal mu-calculus is an extension of the mu-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property that can be expressed in this logic can be checked in polynomial time, and conversely every polynomial-time decidable problem that has a bisimulation-invariant encoding into labeled transition systems can also be defined in the higher-dimensional modal mu-calculus. We exemplify the latter connection by giving several examples of decision problems which reduce to model checking of the higher-dimensional modal mu-calculus for some fixed formulas. This way generic model checking algorithms for the logic can then be used via partial evaluation in order to obtain algorithms for theses problems which may benefit from improvements that are well-established in the field of program verification, namely on-the-fly and symbolic techniques. The aim of this work is to extend such techniques to other fields as well, here exemplarily done for process equivalences, automata theory, parsing, string problems, and games. △ Less

Submitted 15 February, 2012; originally announced February 2012.

Comments: In Proceedings FICS 2012, arXiv:1202.3174

ACM Class: F.4.1, F.2.m, F.3.0

Journal ref: EPTCS 77, 2012, pp. 39-46

Separability in the Ambient Logic

Authors: Daniel Hirschkoff, Etienne Lozes, Davide Sangiorgi

Abstract: The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on processes induced by the logic $(=_L>)$. As underlying calculi besides MA we consider a subcalculus in… ▽ More The \it{Ambient Logic} (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the discriminating power of AL, focusing on the equivalence on processes induced by the logic $(=_L>)$. As underlying calculi besides MA we consider a subcalculus in which an image-finiteness condition holds and that we prove to be Turing complete. Synchronous variants of these calculi are studied as well. In these calculi, we provide two operational characterisations of $_=L$: a coinductive one (as a form of bisimilarity) and an inductive one (based on structual properties of processes). After showing $_=L$ to be stricly finer than barbed congruence, we establish axiomatisations of $_=L$ on the subcalculus of MA (both the asynchronous and the synchronous version), enabling us to relate $_=L$ to structural congruence. We also present some (un)decidability results that are related to the above separation properties for AL: the undecidability of $_=L$ on MA and its decidability on the subcalculus. △ Less

Submitted 4 September, 2008; v1 submitted 24 June, 2008; originally announced June 2008.

Comments: logical methods in computer science, 44 pages

ACM Class: F.3.2; F.4.1

Journal ref: Logical Methods in Computer Science, Volume 4, Issue 3 (September 4, 2008) lmcs:682

On the Expressiveness of the Ambient Logic

Authors: Daniel Hirschkoff, Etienne Lozes, Davide Sangiorgi

Abstract: The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture finitess of a term, name occurrences and persistence.… ▽ More The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We define formulas for capabilities and for communication in MA. We also derive some formulas that capture finitess of a term, name occurrences and persistence. We study extensions of the calculus involving more complex forms of communications, and we define characteristic formulas for the equivalence induced by the logic on a subcalculus of MA. This subcalculus is defined by imposing an image-finiteness condition on the reducts of a MA process. △ Less

Submitted 30 March, 2006; v1 submitted 4 October, 2005; originally announced October 2005.

ACM Class: F.4.3

Journal ref: Logical Methods in Computer Science, Volume 2, Issue 2 (March 30, 2006) lmcs:2251