This volume contains the proceedings of the 12th International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2021). The aim of GandALF 2021 symposium is to bring together researchers from academia and industry which are activel
y working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization.
In this paper, emph{diagnosability} is characterized for a labeled max-plus automaton $mathcal{A}^{mathcal{D}}$ over a dioid $mathcal{D}$ as a real-time system. In order to represent time elapsing, a special class of dioids called emph{progressive} a
re considered, in which there is a total canonical order, there is at least one element greater than $textbf{1}$, the product of sufficiently many elements greater than $textbf{1}$ is arbitrarily large, and the cancellative law is satisfied. Then a notion of diagnosability is formulated for $mathcal{A}^{mathcal{D}}$ over a progressive dioid $mathcal{D}$. By developing a notion of emph{concurrent composition}, a sufficient and necessary condition is given for diagnosability of automaton $mathcal{A}^{mathcal{D}}$. It is also proven that the problem of verifying diagnosability of $mathcal{A}^{underline{mathbb{Q}}}$ is coNP-complete, where coNP-hardness even holds for deterministic, deadlock-free, and divergence-free $mathcal{A}^{underline{mathbb{N}}}$, where $underline{mathbb{Q}}$ and $underline{mathbb{N}}$ are the max-plus dioids having elements in $mathbb{Q}cup{-infty}$ and $mathbb{N}cup{-infty}$, respectively.
In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and contex
t-free grammars, most of the usual problems (reachability, coverability, finiteness, boundedness and termination) were known to be solvable by using non-primitive recursive algorithms. For almost all other extended Petri nets models containing a stack, the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability, termination, boundedness and finiteness problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get a more powerful model than Petri net for free.
Spell checking and morphological analysis are two fundamental tasks in text and natural language processing and are addressed in the early stages of the development of language technology. Despite the previous efforts, there is no progress in open-so
urce to create such tools for Sorani Kurdish, also known as Central Kurdish, as a less-resourced language. In this paper, we present our efforts in annotating a lexicon with morphosyntactic tags and also, extracting morphological rules of Sorani Kurdish to build a morphological analyzer, a stemmer and a spell-checking system using Hunspell. This implementation can be used for further developments in the field by researchers and also, be integrated into text editors under a publicly available license.
We prove that the genus of a regular language is decidable. For this purpose, we use a graph-theoretical approach. We show that the original question is equivalent to the existence of a special kind of graph epimorphism - a directed emulator morphism
-- onto the underlying graph of the minimal deterministic automaton for the regular language. We also prove that the class of directed emulators of genus less than or equal to $g$ is closed under minors. Decidability follows from the Robertson-Seymour theorem.
Higher-order constrained Horn clauses (HoCHC) are a semantically-invariant system of higher-order logic modulo theories. With semi-decidable unsolvability over a semi-decidable background theory, HoCHC is suitable for safety verification. Less is kno
wn about its relation to larger classes of higher-order verification problems. Motivated by program equivalence, we introduce a coinductive version of HoCHC that enjoys a greatest model property. We define an encoding of higher-order recursion schemes (HoRS) into HoCHC logic programs. Correctness of this encoding reduces decidability of the open HoRS equivalence problem -- and, thus, the LambdaY-calculus Bohm tree equivalence problem -- to semi-decidability of coinductive HoCHC over a complete and decidable theory of trees.
In this paper, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees for an input string i
n linear time. Each parse tree in the forest can then be extracted also in linear time. Besides the parser generator, to allow more flexible forms of the visibly pushdown grammars, we also present a translator that converts a tagged CFG to a visibly pushdown grammar in a sound way, and the parse trees of the tagged CFG are further produced by running the semantic actions embedded in the parse trees of the translated visibly pushdown grammar. The performance of the parser is compared with a popular parsing tool ANTLR and other popular hand-crafted parsers. The correctness of the core parsing algorithm is formally verified in the proof assistant Coq.
We investigate the problem of parameter synthesis for time Petri nets with a cost variable that evolves both continuously with time, and discretely when firing transitions. More precisely, parameters are rational symbolic constants used for time cons
traints on the firing of transitions and we want to synthesise all their values such that some marking is reachable, with a cost that is either minimal or simply less than a given bound. We first prove that the mere existence of values for the parameters such that the latter property holds is undecidable. We nonetheless provide symbolic semi-algorithms for the two synthesis problems and we prove them both sound and complete when they terminate. We also show how to modify them for the case when parameter values are integers. Finally, we prove that these modifi
In the classical synthesis problem, we are given an LTL formula psi over sets of input and output signals, and we synthesize a system T that realizes psi: with every input sequences x, the system associates an output sequence T(x) such that the gener
ated computation x otimes T(x) satisfies psi. In practice, the requirement to satisfy the specification in all environments is often too strong, and it is common to add assumptions on the environment. We introduce a new type of relaxation on this requirement. In good-enough synthesis (GE-synthesis), the system is required to generate a satisfying computation only if one exists. Formally, an input sequence x is hopeful if there exists some output sequence y such that the computation x otimes y satisfies psi, and a system GE-realizes psi if it generates a computation that satisfies psi on all hopeful input sequences. GE-synthesis is particularly relevant when the notion of correctness is multi-valued (rather than Boolean), and thus we seek systems of the highest possible quality, and when synthesizing autonomous systems, which interact with unexpected environments and are often only expected to do their best. We study GE-synthesis in Boolean and multi-valued settings. In both, we suggest and solve various definitions of GE-synthesis, corresponding to different ways a designer may want to take hopefulness into account. We show that in all variants, GE-synthesis is not computationally harder than traditional synthesis, and can be implemented on top of existing tools. Our algorithms are based on careful combinations of nondeterministic and universal automata. We augment systems that GE-realize their specifications by monitors that provide satisfaction information. In the multi-valued setting, we provide both a worst-case analysis and an expectation-based one, the latter corresponding to an interaction with a stochastic environment.
Reinforcement learning (RL) is a promising approach and has limited success towards real-world applications, because ensuring safe exploration or facilitating adequate exploitation is a challenges for controlling robotic systems with unknown models a
nd measurement uncertainties. Such a learning problem becomes even more intractable for complex tasks over continuous space (state-space and action-space). In this paper, we propose a learning-based control framework consisting of several aspects: (1) linear temporal logic (LTL) is leveraged to facilitate complex tasks over an infinite horizons which can be translated to a novel automaton structure; (2) we propose an innovative reward scheme for RL-agent with the formal guarantee such that global optimal policies maximize the probability of satisfying the LTL specifications; (3) based on a reward shaping technique, we develop a modular policy-gradient architecture utilizing the benefits of automaton structures to decompose overall tasks and facilitate the performance of learned controllers; (4) by incorporating Gaussian Processes (GPs) to estimate the uncertain dynamic systems, we synthesize a model-based safeguard using Exponential Control Barrier Functions (ECBFs) to address problems with high-order relative degrees. In addition, we utilize the properties of LTL automatons and ECBFs to construct a guiding process to further improve the efficiency of exploration. Finally, we demonstrate the effectiveness of the framework via several robotic environments. And we show such an ECBF-based modular deep RL algorithm achieves near-perfect success rates and guard safety with a high probability confidence during training.
