Author name cluster

Étienne Lozes

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

TIME Conference 2022 Conference Paper

The Tail-Recursive Fragment of Timed Recursive CTL

Florian Bruse
Martin Lange 0001
Étienne Lozes

Timed Recursive CTL (TRCTL) was recently proposed as a merger of two extensions of the well-known branching-time logic CTL: Timed CTL on one hand is interpreted over real-time systems like timed automata, and Recursive CTL (RecCTL) on the other hand obtains high expressiveness through the introduction of a recursion operator. Model checking for the resulting logic is known to be 2-EXPTIME-complete. The aim of this paper is to investigate the possibility to obtain a fragment of lower complexity without losing too much expressive power. It is obtained by a syntactic property called "tail-recursiveness" that restricts the way that recursive formulas can be built. This restriction is known to decrease the complexity of model checking by half an exponential in the untimed setting. We show that this also works in the real-time world: model checking for the tail-recursive fragment of TRCTL is EXPSPACE-complete. The upper bound is obtained by a standard untiming construction via region graphs, and rests on the known complexity of tail-recursive fragments of higher-order modal logics. The lower bound is established by a reduction from a suitable tiling problem.

Details

CSL Conference 2020 Conference Paper

Internal Calculi for Separation Logics

Stéphane Demri
Étienne Lozes
Alessio Mansutti

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 SL(∗, -*). 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.

Details

I&C Journal 2018 Journal Article

Multi-buffer simulations: Decidability and complexity

Milka Hutagalung
Norbert Hundeshagen
Dietrich Kuske
Martin Lange
Étienne Lozes

Multi-buffer simulation is a refinement of fair simulation between two nondeterministic Büchi automata (NBA). It is characterised by a game in which letters get pushed to and taken from FIFO buffers of bounded or unbounded capacity. Games with a single buffer approximate the PSPACE-complete language inclusion problem for NBA. With multiple buffers and a fixed mapping of letters to buffers these games approximate the undecidable inclusion problem between Mazurkiewicz trace languages. We study the decidability and complexity of multi-buffer simulations and obtain the following results: P-completeness for fixed bounded buffers, EXPTIME-completeness in case of a single unbounded buffer and high undecidability (in the analytic hierarchy) with two buffers of which at least one is unbounded. We also consider a variant in which the buffers are kept untouched or flushed and show PSPACE-completeness for the single-buffer case.

Details DOI

CSL Conference 2008 Conference Paper

On the Almighty Wand

Rémi Brochenin
Stéphane Demri
Étienne Lozes

Abstract We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL ) and its fragments. SL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as SL and as a by-product we get undecidability of SL. This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. As a consequence of this deep result, in SL the magic wand can simulate the separating conjunction. By contrast, we establish that SL without the magic wand is decidable with non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. Equivalence between second-order logic and separation logic extends to the case with more than one selector.

Details

TCS Journal 2005 Journal Article

Elimination of spatial connectives in static spatial logics

Étienne Lozes

The recent interest for specification on resources yields so-called spatial logics, that is specification languages offering new forms of reasoning: the local reasoning through the separation of the resource space into two disjoint subspaces, and the contextual reasoning through hypothetical extension of the resource space. We consider two resource models and their related logics: • The static ambient model, proposed as an abstraction of semistructured data (Proc. ESOP’01, Lecture Notes in Computer Science, vol. 2028, Springer, Berlin, 2001, pp. 1–22 (invited paper)) with the static ambient logic (SAL) that was proposed as a request language, both obtained by restricting the mobile ambient calculus (Proc. FOSSACS’98, Lecture Notes in Computer Science, vol. 1378, Springer, Berlin, 1998, pp. 140–155) and logic (Proc. POPL’00, ACM Press, New York, 2000, pp. 365–377) to their purely static aspects. • The memory model and the assertion language of separation logic, both defined in Reynolds (Proc. LICS’02, 2002) for the purpose of the axiomatic semantic of imperative programs manipulating pointers. We raise the questions of the expressiveness and the minimality of these logics. Our main contribution is a minimalisation technique we may apply for these two logics. We moreover show some restrictions of this technique for the extension SAL ∀ with universal quantification, and we establish the minimality of the adjunct-free fragment ( SAL int ).

Details DOI