Author name cluster

Marc Zeitoun

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.

7 papers

2 author rows

CSL Conference 2024 Conference Paper

A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic

Thomas Place
Marc Zeitoun

We study an operator on classes of languages. For each class 𝒞, it produces a new class FO²(𝕀_𝒞) associated with a variant of two-variable first-order logic equipped with a signature 𝕀_𝒞 built from 𝒞. For 𝒞 = {∅, A*}, we obtain the usual FO²(<)} logic, equipped with linear order. For 𝒞 = {∅, {ε}, A+, A*}, we get the variant FO²(<, +1), which also includes the successor predicate. If 𝒞 consists of all Boolean combinations of languages A*aA*, where a is a letter, we get the variant FO²(<, Bet), which includes "between" relations. We prove a generic algebraic characterization of the classes FO^2(𝕀_𝒞). It elegantly generalizes those known for all the cases mentioned above. Moreover, it implies that if 𝒞 has decidable separation (plus some standard properties), then FO²2(𝕀_𝒞) has a decidable membership problem. We actually work with an equivalent definition of FO²(𝕀_𝒞) in terms of unary temporal logic. For each class 𝒞, we consider a variant TL(𝒞) of unary temporal logic whose future/past modalities depend on 𝒞 and such that TL(𝒞) = FO²(𝕀_𝒞). Finally, we also characterize FL(𝒞) and PL(𝒞), the pure-future and pure-past restrictions of TL(𝒞). Like for TL(𝒞), these characterizations imply that if 𝒞 is a class with decidable separation, then FL(𝒞) and PL(𝒞) have decidable membership.

Details

Highlights Conference 2024 Conference Abstract

Decision problems for regular languages

Marc Zeitoun

Given a class of regular languages, the C-membership problem asks whether a given regular language belongs to C. While most questions about automata are well understood today, the C-membership problem remains open for several significant classes, in particular for most levels of the quantifier alternation hierarchy in first-order logic. This talk will present approaches to solving this problem, aimed at simultaneously capturing several variants of a specific level.

Details

MFCS Conference 2016 Conference Paper

The Covering Problem: A Unified Approach for Investigating the Expressive Power of Logics

Thomas Place
Marc Zeitoun

An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the membership problem, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the "right" one by the seminal work of Schuetzenberger, McNaughton and Papert on first-order logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of first-order logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been ad hoc, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem.

Details

Highlights Conference 2013 Conference Abstract

Separating regular languages by piecewise testable and unambiguous languages

Thomas Place
Lorijn van Rooijen
Marc Zeitoun

We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a $\mathcal{B}\Sigma_1(<)$ sentence can witness that the languages are disjoint. If this is possible, we express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can also decide whether two regular languages can be separated by an unambiguous (i. e. $FO^2(<)$-definable) language, albeit with a higher complexity.

PDF Details

MFCS Conference 2013 Conference Paper

Separating Regular Languages by Piecewise Testable and Unambiguous Languages

Thomas Place
Lorijn van Rooijen
Marc Zeitoun

Abstract Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from another class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a $\mathcal{B}\Sigma_1(<)$ sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity.

Details

MFCS Conference 2011 Conference Paper

Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking

Benedikt Bollig
Aiswarya Cyriac
Paul Gastin
Marc Zeitoun

Abstract We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and that, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.

Details

TCS Journal 2007 Journal Article

An automata-theoretic approach to the word problem for ω -terms over R

Jorge Almeida
Marc Zeitoun

This paper studies the pseudovariety R of all finite R -trivial semigroups. We give a representation of pseudowords over R by infinite trees, called R -trees. Then we show that a pseudoword is an ω -term if and only if its associated tree is regular (i. e. it can be folded into a finite graph), or equivalently, if the ω -term has a finite number of tails. We give a linear algorithm to compute a compact representation of the R -tree for ω -terms, which yields a linear solution of the word problem for ω -terms over R. We finally exhibit a basis for the ω -variety generated by R and we show that there is no finite basis. Several results can be compared to recent work of Bloom and Choffrut on long words.

Details DOI