形式语言与自动机理论

We give an upper bound of $n((n-1)!-(n-3)!)$ for the possible largest size of a subsemigroup of the full transformational semigroup over $n$ elements consisting only of nonpermutational transformations. As an application we gain the same…

Scenarios, or Message Sequence Charts, offer an intuitive way of describing the desired behaviors of a distributed protocol. In this paper we propose a new way of specifying finite-state protocols using scenarios: we show that it is…

Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of…

A register automaton is a finite automaton with finitely many registers ranging from an infinite alphabet. Since the valuations of registers are infinite, there are infinitely many configurations. We describe a technique to classify…

The paper shows that there is a deep structure on certain sets of bisimilar Probabilistic Automata (PA). The key prerequisite for these structures is a notion of compactness of PA. It is shown that compact bisimilar PA form lattices. These…

This volume contains the proceedings of Infinity'13, the 15th International Workshop on Verification of Infinite-State Systems, which was held in Hanoi, Vietnam on the 14th of October 2013 as a satellite event of ATVA'13. The aim of the…

We study the density of periodic configurations for shift spaces defined on (the Cayley graph of) a finitely generated group. We prove that in the case of a full shift on a residually finite group and in that of a group shift space on an…

In this paper we study the word problem of groups corresponding to tessellations of the hyperbolic plane. In particular using the Fibonacci technology developed by the second author we show that groups corresponding to the pentagrid or the…

The understanding of Boolean automata networks dynamics takes an important place in various domains of computer science such as computability, complexity and discrete dynamical systems. In this paper, we make a step further in this…

Cellular automata are discrete dynamical systems and a model of computation. The limit set of a cellular automaton consists of the configurations having an infinite sequence of preimages. It is well known that these always contain a…

We study the problem of revising specifications with preferences for automata based control synthesis problems. In this class of revision problems, the user provides a numerical ranking of the desirability of the subgoals in their…

Context-Free Grammars (CFGs) and Parsing Expression Grammars (PEGs) have several similarities and a few differences in both their syntax and semantics, but they are usually presented through formalisms that hinder a proper comparison. In…

Most scripting languages nowadays use regex pattern-matching libraries. These regex libraries borrow the syntax of regular expressions, but have an informal semantics that is different from the semantics of regular expressions, removing the…

Parsing Expression Grammars (PEGs) are a formalism that can describe all deterministic context-free languages through a set of rules that specify a top-down parser for some language. PEGs are easy to use, and there are efficient…

Mazurkiewicz traces describe concurrent behaviors of distributed systems. Trace-closed word languages, which are "linearizations" of trace languages, constitute a weaker notion of concurrency but still give us tools to investigate the…

We focus on (partial) functions that map input strings to a monoid such as the set of integers with addition and the set of output strings with concatenation. The notion of regularity for such functions has been defined using two-way…

We study the sofic tree shifts of $A^{\Sigma^*}$, where $\Sigma^*$ is a regular rooted tree of finite rank. In particular, we give their characterization in terms of unrestricted Rabin automata. We show that if $X \subset A^{\Sigma^*}$ is a…

We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we…

Champarnaud and Ziadi, and Khorsi et al. show how to compute the equation automaton of word regular expression $E$ via the $k$-C-Continuations. Kuske and Meinecke extend the computation of the equation automaton to a regular tree expression…

In this paper we consider word equations with one variable (and arbitrary many appearances of it). A recent technique of recompression, which is applicable to general word equations, is shown to be suitable also in this case. While in…