SU\G(𝔸)/K·U
Sign Up for free Log In

Alternating Nominal Automata with Name Allocation

Authors

Florian Frank, Daniel Hausmann, Stefan Milius, Lutz Schröder, Henning Urbat
Type: Preprint
Publication Date: 2024-08-07
Citations: 0
DOI: https://doi.org/10.48550/arxiv.2408.03658

Abstract

Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state.

Locations

  • arXiv (Cornell University)
    View PDF

Ask a Question About This Paper

Summary

Login to see paper summary

Nominal Tree Automata With Name Allocation

2024-05-23
Simon Prucker , Lutz Schröder
Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering … Data trees serve as an abstraction of structured data, such as XML documents. A number of specification formalisms for languages of data trees have been developed, many of them adhering to the paradigm of register automata, which is based on storing data values encountered on the tree in registers for subsequent comparison with further data values. Already on word languages, the expressiveness of such automata models typically increases with the power of control (e.g. deterministic, non-deterministic, alternating). Language inclusion is typically undecidable for non-deterministic or alternating models unless the number of registers is radically restricted, and even then often remains non-elementary. We present an automaton model for data trees that retains a reasonable level of expressiveness, in particular allows non-determinism and any number of registers, while admitting language inclusion checking in elementary complexity, in fact in parametrized exponential time. We phrase the description of our automaton model in the language of nominal sets, building on the recently introduced paradigm of explicit name allocation in nominal automata.
Chat View PDF

A Linear-Time Nominal $\mu$-Calculus with Name Allocation

2020-10-21
Daniel Hausmann , Stefan Milius , Lutz Schröder
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms … Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-muTL for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-muTL allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-muTL over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.

A Linear-Time Nominal $μ$-Calculus with Name Allocation

2020-01-01
Daniel Hausmann , Stefan Milius , Lutz Schröder
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms … Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, such as nondetermininistic orbit-finite automata (NOFAs), where names play the role of data. Reasoning problems in such formalisms tend to be computationally hard. Name-binding nominal automata models such as regular nondeterministic nominal automata (RNNAs) have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-muTL for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to extended regular nondeterministic nominal automata that even though Bar-muTL allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-muTL over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.
Chat View PDF

Nominal Büchi Automata with Name Allocation

2021-01-01
Henning Urbat , Daniel Hausmann , Stefan Milius +1 more
Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach omega-languages over infinite alphabets in the … Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach omega-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.
Chat View PDF

Nominal Regular Expressions for Languages over Infinite Alphabets. Extended Abstract

2013-01-01
Alexander Kurz , Tomoyuki Suzuki , Emilio Tuosto
We propose regular expressions to abstractly model and study properties of resource-aware computations. Inspired by nominal techniques -- as those popular in process calculi -- we extend classical regular expressions … We propose regular expressions to abstractly model and study properties of resource-aware computations. Inspired by nominal techniques -- as those popular in process calculi -- we extend classical regular expressions with names (to model computational resources) and suitable operators (for allocation, deallocation, scoping of, and freshness conditions on resources). We discuss classes of such nominal regular expressions, show how such expressions have natural interpretations in terms of languages over infinite alphabets, and give Kleene theorems to characterise their formal languages in terms of nominal automata.
Chat View PDF

Harnessing LTL With Freeze Quantification

2020-10-21
Daniel Hausmann , Stefan Milius , Lutz Schröder
Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, respectively, serve the verification of processes or documents with data. They relate tightly to … Logics and automata models for languages over infinite alphabets, such as Freeze LTL and register automata, respectively, serve the verification of processes or documents with data. They relate tightly to formalisms over nominal sets, where names play the role of data. For example, regular nondeterministic nominal automata (RNNA) are equivalent to a subclass of the standard register automata model, characterized by a lossiness condition referred to as name dropping. This subclass generally enjoys better computational properties than the full class of register automata, for which, e.g., inclusion checking is undecidable. Similarly, satisfiability in full freeze LTL is undecidable, and decidable but not primitive recursive if the number of registers is limited to at most one. In the present paper, we introduce a name-dropping variant bar-muTL of Freeze LTL for finite words over an infinite alphabet. We show by reduction to extended regular nondeterministic nominal automata (ERNNA) that even with unboundedly many registers, model checking for bar-muTL over RNNA is elementary, in fact in ExpSpace, more precisely in parametrized PSpace, effectively with the number of registers as the parameter.

History-Register Automata

2016-03-29
Radu Grigore , Nikos Tzevelekos
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic … Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
Chat View PDF

Nominal Automata with Name Binding

2017-01-01
Lutz Schröder , Dexter Kozen , Stefan Milius +1 more
Chat View PDF

Residual Nominal Automata

2019-10-25
Joshua Moerman , Matteo Sammartino
Nominal automata are models for accepting languages over infinite alphabets. In this paper we refine the hierarchy of nondeterministic nominal automata, by developing the theory of residual nominal automata. In … Nominal automata are models for accepting languages over infinite alphabets. In this paper we refine the hierarchy of nondeterministic nominal automata, by developing the theory of residual nominal automata. In particular, we show that they admit canonical minimal representatives, and that the universality problem becomes decidable. We also study exact learning of these automata, and settle questions that were left open about their learnability via observations.
Chat View PDF

Register Set Automata (Technical Report)

2022-01-01
Sabína Gulčíková , Ondřej Lengál
We present register set automata (RsAs), a register automaton model over data words where registers can contain sets of data values and the following operations are supported: adding values to … We present register set automata (RsAs), a register automaton model over data words where registers can contain sets of data values and the following operations are supported: adding values to registers, clearing registers, and testing (non-)membership. We show that the emptiness problem for RsAs is decidable and complete for the $F_\omega$ class. Moreover, we show that a large class of register automata can be transformed into deterministic RsAs, which can serve as a basis for (i) fast matching of a family of regular expressions with back-references and (ii) language inclusion algorithm for a sub-class of register automata. RsAs are incomparable in expressive power to other popular automata models over data words, such as alternating register automata and pebble automata.
Chat View PDF

Synthesis over Regularly Approximable Data Domains.

2021-10-17
Léo Exibard , Emmanuel Filiot , Ayrat Khalimov
We study reactive synthesis of systems interacting with environments using infinite alphabets. Register automata and transducers are popular formalisms for specifying and modelling such systems. They extend finite-state automata by … We study reactive synthesis of systems interacting with environments using infinite alphabets. Register automata and transducers are popular formalisms for specifying and modelling such systems. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. Its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is however known to be decidable for universal register automata which can compare data for equality. In this paper, we generalise this result. We introduce the notion of $\omega$-regularly approximable data domains, and show that register-bounded synthesis from universal register automata on such domains is decidable. Importantly, the data domain ($\mathbb{N}$, =, <) with natural order is $\omega$-regularly approximable, and its closer examination reveals that the synthesis problem is decidable in time doubly exponential in the number of registers, matching the known complexity of the equality-only case ($\mathbb{N}$, =). We then introduce a notion of reducibility between data domains which we exploit to show decidability of synthesis over, e.g., the domains ($\mathbb{N}^d$, $=^d$, $<^d$) of tuples of numbers equipped with the component-wise partial order and ($\Sigma^*$, =, $\prec$) of finite strings with the prefix relation.

Coalgebraic Semantics for Nominal Automata

2022-01-01
Florian Frank , Stefan Milius , Henning Urbat
This paper provides a coalgebraic approach to the language semantics of two types of non-deterministic automata over nominal sets: non-deterministic orbit-finite automata (NOFAs) and regular nominal non-deterministic automata (RNNAs), which … This paper provides a coalgebraic approach to the language semantics of two types of non-deterministic automata over nominal sets: non-deterministic orbit-finite automata (NOFAs) and regular nominal non-deterministic automata (RNNAs), which were introduced in previous work. While NOFAs are a straightforward nominal version of non-deterministic automata, RNNAs feature ordinary as well as name binding transitions. Correspondingly, words accepted by RNNAs are strings formed by ordinary letters and name binding letters. Bar languages are sets of such words modulo $\alpha$-equivalence, and to every state of an RNNA one associates its accepted bar language. We show that the semantics of NOFAs and RNNAs, respectively, arise both as an instance of the Kleisli-style coalgebraic trace semantics as well as an instance of the coalgebraic language semantics obtained via generalized determinization. On the way we revisit coalgebraic trace semantics in general and give a new compact proof for the main result in that theory stating that an initial algebra for a functor yields the terminal coalgebra for the Kleisli extension of the functor. Our proof requires fewer assumptions on the functor than all previous ones.
Chat View PDF

Relating timed and register automata

2010-11-27
Diego Figueira , Piotr Hofman , Sławomir Lasota
Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two … Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance. This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. Our results allow to transfer complexity and decidability results back and forth between these two kinds of models. We justify the usefulness of these reductions by obtaining new results on register automata.
Chat View PDF

Relating timed and register automata

2014-12-05
Diego Figueira , Piotr Hofman , Sławomir Lasota
Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two … Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance. This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. Our results allow to transfer complexity and decidability results back and forth between these two kinds of models. We justify the usefulness of these reductions by obtaining new results on register automata.
Chat View PDF

{\omega}-Automata

2016-09-10
Thomas Wilke
This paper gives a concise introduction into the basic theory of {\omega}-automata (as of March 2014). The starting point are the different types of recurrence conditions, modes of operation (deterministic, … This paper gives a concise introduction into the basic theory of {\omega}-automata (as of March 2014). The starting point are the different types of recurrence conditions, modes of operation (deterministic, nondeterministic, alternating automata), and directions (forward or backward automata). The main focus is on fundamental automata constructions, for instance, for boolean operations, determinization, disambiguation, and removing alternation. It also covers some algebraic aspects such as congruences for {\omega}-automata (and {\omega}-languages), basic structure theory (loops), and applications in mathematical logic. This paper may eventually become a chapter in a handbook of automata theory.
Chat View PDF

Nominal Automata with Name Binding

2016-03-04
Lutz Schröder , Dexter Kozen , Stefan Milius +1 more
Automata models for data languages (i.e. languages over infinite alphabets) often feature either global or local freshness operators. We show that Bollig et al.'s session automata, which focus on global … Automata models for data languages (i.e. languages over infinite alphabets) often feature either global or local freshness operators. We show that Bollig et al.'s session automata, which focus on global freshness, are equivalent to regular nondeterministic nominal automata (RNNA), a natural nominal automaton model with explicit name binding that has appeared implicitly in the semantics of nominal Kleene algebra (NKA), an extension of Kleene algebra with name binding. The expected Kleene theorem for NKA is known to fail in one direction, i.e. there are nominal languages that can be accepted by an RNNA but are not definable in NKA; via session automata, we obtain a full Kleene theorem for RNNAs for an expression language that extends NKA with unscoped name binding. Based on the equivalence with RNNAs, we then slightly rephrase the known equivalence checking algorithm for session automata. Reinterpreting the data language semantics of name binding by unrestricted instead of clean alpha-equivalence, we obtain a local freshness semantics as a quotient of the global freshness semantics. Under local freshness semantics, RNNAs turn out to be equivalent to a natural subclass of Bojanczyk et al.'s nondeterministic orbit-finite automata. We establish decidability of inclusion under local freshness by modifying the RNNA-based algorithm; in summary, we obtain a formalism for local freshness in data languages that is reasonably expressive and has a decidable inclusion problem.
Chat View PDF

Nominal Automata with Name Binding

2016-01-01
Lutz Schröder , Dexter Kozen , Stefan Milius +1 more
Automata models for data languages (i.e. languages over infinite alphabets) often feature either global or local freshness operators. We show that Bollig et al.'s session automata, which focus on global … Automata models for data languages (i.e. languages over infinite alphabets) often feature either global or local freshness operators. We show that Bollig et al.'s session automata, which focus on global freshness, are equivalent to regular nondeterministic nominal automata (RNNA), a natural nominal automaton model with explicit name binding that has appeared implicitly in the semantics of nominal Kleene algebra (NKA), an extension of Kleene algebra with name binding. The expected Kleene theorem for NKA is known to fail in one direction, i.e. there are nominal languages that can be accepted by an RNNA but are not definable in NKA; via session automata, we obtain a full Kleene theorem for RNNAs for an expression language that extends NKA with unscoped name binding. Based on the equivalence with RNNAs, we then slightly rephrase the known equivalence checking algorithm for session automata. Reinterpreting the data language semantics of name binding by unrestricted instead of clean alpha-equivalence, we obtain a local freshness semantics as a quotient of the global freshness semantics. Under local freshness semantics, RNNAs turn out to be equivalent to a natural subclass of Bojanczyk et al.'s nondeterministic orbit-finite automata. We establish decidability of inclusion under local freshness by modifying the RNNA-based algorithm; in summary, we obtain a formalism for local freshness in data languages that is reasonably expressive and has a decidable inclusion problem.
Chat View PDF

Symbolic Register Automata

2018-01-01
Loris D’Antoni , Tiago Ferreira , Matteo Sammartino +1 more
Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a … Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.
Chat View PDF

Symbolic Register Automata

2018-11-16
Loris D’Antoni , Tiago Ferreira , Matteo Sammartino +1 more
Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a … Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.

Automata theory in nominal sets

2014-08-15
Mikołaj Bojańczyk , Bartek Klin , Sławomir Lasota
We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, … We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.
Chat View PDF