Latest in cs.fl

total 2722took 0.13s
On substitutions closed under derivation: examplesJul 12 2019We study infinite words fixed by a morphism and their derived words. A derived word is a coding of return words to a factor. We exhibit two examples of sets of morphisms which are closed under derivation --- any derived word with respect to any factor ... More
Visualização e animação de autómatos em Ocsigen FrameworkJul 11 2019Formal Languages and Automata Theory are important foundational topics in Computer Science. Their rigorous and formal characteristics make their learning them demanding. An important support for the assimilation of concepts is the possibility of interactively ... More
Time-aware uniformization of winning strategiesJul 11 2019Two-player win/lose games of infinite duration are involved in several disciplines including computer science and logic. If such a game has deterministic winning strategies, one may ask how simple such strategies can get. The answer may help with actual ... More
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple FormulasJul 11 2019HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental ... More
String Attractors and Combinatorics on WordsJul 10 2019The notion of \emph{string attractor} has recently been introduced in [Prezza, 2017] and studied in [Kempa and Prezza, 2018] to provide a unifying framework for known dictionary-based compressors. A string attractor for a word $w=w[1]w[2]\cdots w[n]$ ... More
A duality theoretic view on limits of finite structuresJul 09 2019The study of limits of sequences of finite structures plays a crucial role in finite model theory. It is motivated by an attempt to understand the behaviour of dynamical systems, such as computer networks evolving over time. For this purpose, starting ... More
fbSAT: Automatic Inference of Minimal Finite-State Models of Function BlocksJul 07 2019Finite-state models are widely used in software engineering, especially in control systems development. Commonly, in control applications such models are developed manually, hence, keeping them up-to-date requires extra effort. To simplify the maintenance ... More
Nonuniform Families of Polynomial-Size Quantum Finite Automata and Quantum Logarithmic-Space Computation with Polynomial-Size AdviceJul 05 2019The state complexity of a finite(-state) automaton intuitively measures the size of the description of the automaton. Sakoda and Sipser [STOC 1972, pp. 275-286] were concerned with nonuniform families of finite automata and they discussed the behaviors ... More
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating AutomataJul 05 2019This paper proposes a new algorithm for the generation of unambiguous B\"uchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. ... More
Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vousJul 05 2019We present in this paper a generic framework for the analysis of multi-threaded programs with recursive procedure calls, synchronisation by rendez-vous between parallel threads, and dynamic creation of new threads. To this end, we consider a model called ... More
On The Structure of Dyck LanguagesJul 04 2019We prove that the closure of the one-sided Dyck language in a free monoid is a two-sided Dyck language.
Revisiting local time semantics for networks of timed automataJul 04 2019We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion ... More
Computing Probabilistic Bisimilarity Distances for Probabilistic AutomataJul 03 2019Jul 04 2019The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity ... More
Computing Probabilistic Bisimilarity Distances for Probabilistic AutomataJul 03 2019The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity ... More
What's decidable about parametric timed automata?Jul 03 2019Parametric timed automata (PTAs) are a powerful formalism to reason, simulate and formally verify critical real-time systems. After 25 years of research on PTAs, it is now well-understood that any non-trivial problem studied is undecidable for general ... More
Acceptance Ambiguity for Quantum AutomataJul 02 2019We consider notions of freeness and ambiguity for the acceptance probability of Moore-Crutchfield Measure Once Quantum Finite Automata (MO-QFA). We study the distribution of acceptance probabilities of such MO-QFA, which is partly motivated by similar ... More
The carry propagation of the successor functionJul 02 2019Given any numeration system, we call carry propagation at a number $N$ the number of digits that are changed when going from the representation of $N$ to the one of $N+1$, and amortized carry propagation the limit of the mean of the carry propagations ... More
Timed Basic Parallel ProcessesJul 02 2019Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such ... More
Logics for Reversible Regular Languages and Semigroups with InvolutionJul 02 2019We present MSO and FO logics with predicates `between' and `neighbour' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and ... More
Kleene Theorems for Free Choice Nets Labelled with Distributed AlphabetsJul 02 2019We provided (PNSE'2014) expressions for free choice nets having "distributed choice property" which makes the nets "direct product" representable. In a recent work (PNSE'2016), we gave equivalent syntax for a larger class of free choice nets obtained ... More
The Polynomial Complexity of Vector Addition Systems with StatesJul 01 2019Vector addition systems are an important model in theoretical computer science and have been used in a variety of areas. In this paper, we consider vector addition systems with states over a parameterized initial configuration. For these systems, we are ... More
Typed lambda-calculi and superclasses of regular functionsJun 30 2019We propose to use Church encodings in typed lambda-calculi as the basis for an automata-theoretic counterpart of implicit computational complexity, in the same way that monadic second-order logic provides a counterpart to descriptive complexity. Specifically, ... More
Deciding Memory Safety for Forest DatastructuresJun 29 2019Memory safety is the problem of determining if a heap manipulating program that allocates/frees memory locations and manipulates heap pointers, does not dereference a memory location that is not allocated. Memory safety errors are serious security vulnerabilities ... More
Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted AutomataJun 28 2019Monitoring of a signal plays an essential role in the runtime verification of cyber-physical systems. Qualitative timed pattern matching is one of the mathematical formulations of monitoring, which gives a Boolean verdict for each sub-signal according ... More
On Solving Word Equations Using SATJun 27 2019We present Woorpje, a string solver for bounded word equations (i.e., equations where the length of each variable is upper bounded by a given integer). Our algorithm works by reformulating the satisfiability of bounded word equations as a reachability ... More
Good for Games Automata: From Nondeterminism to AlternationJun 27 2019Jun 28 2019A word automaton recognizing a language $L$ is good for games (GFG) if its composition with any game with winning condition $L$ preserves the game's winner. While all deterministic automata are GFG, some nondeterministic automata are not. There are various ... More
Good for Games Automata: From Nondeterminism to AlternationJun 27 2019A word automaton recognizing a language $L$ is good for games (GFG) if its composition with any game with winning condition $L$ preserves the game's winner. While all deterministic automata are GFG, some nondeterministic automata are not. There are various ... More
FSM Error MessagesJun 27 2019Computer Science students, in general, find Automata Theory difficult and mostly unrelated to their area of study. To mitigate these perceptions, FSM, a library to program state machines and grammars, was developed to bring programming to the Automata ... More
Approximate Learning of Limit-Average AutomataJun 26 2019Limit-average automata are weighted automata on infinite words that use average to aggregate the weights seen in infinite runs. We study approximate learning problems for limit-average automata in two settings: passive and active. In the passive learning ... More
Pseudo-solutions of word equationsJun 25 2019We present a framework which allows a uniform approach to the recently introduced concept of pseudo-repetitions on words in the morphic case. This framework is at the same time more general and simpler. We introduce the concept of a pseudo-solution and ... More
New Pumping Technique for 2-dimensional VASSJun 25 2019We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting ... More
Efficient Analysis of Unambiguous Automata Using Matrix Semigroup TechniquesJun 24 2019We introduce a novel technique to analyse unambiguous B\"uchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius. ... More
Gray-box Monitoring of Hyperproperties (Extended Version)Jun 20 2019Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. We ... More
A note on Christol's theoremJun 20 2019Christol's theorem characterises algebraic power series over finite fields in terms of finite automata. In a recent article, Bridy develops a new proof of Christol's theorem by Speyer, to obtain a tight quantitative version, that is, to bound the size ... More
On Synthesis of Resynchronizers for TransducersJun 20 2019We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: ... More
On Synthesis of Resynchronizers for TransducersJun 20 2019Jun 24 2019We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: ... More
Computer-Simulation Model Theory (P= NP is not provable)Jun 20 2019The simulation hypothesis says that all the materials and events in the reality (including the universe, our body, our thinking, walking and etc) are computations, and the reality is a computer simulation program like a video game. All works we do (talking, ... More
From Decidability to Undecidability by Considering Regular Sets of InstancesJun 19 2019We are lifting classical problems from single instances to regular sets of instances. The task of finding a positive instance of the combinatorial problem $P$ in a potentially infinite given regular set is equivalent to the so called intreg-problem of ... More
Learning with Partially Ordered RepresentationsJun 19 2019Jun 23 2019This paper examines the characterization and learning of grammars defined with enriched representational models. Model-theoretic approaches to formal language theory traditionally assume that each position in a string belongs to exactly one unary relation. ... More
Learning with Partially Ordered RepresentationsJun 19 2019This paper examines the characterization and learning of grammars defined with enriched representational models. Model-theoretic approaches to formal language theory traditionally assume that each position in a string belongs to exactly one unary relation. ... More
Coverability is Undecidable in One-dimensional Pushdown Vector Addition Systems with ResetsJun 17 2019We consider the model of pushdown vector addition systems with resets. These consist of vector addition systems that have access to a pushdown stack and have instructions to reset counters. For this model, we study the coverability problem. In the absence ... More
Matching Patterns with VariablesJun 17 2019A pattern p (i.e., a string of variables and terminals) matches a word w, if w can be obtained by uniformly replacing the variables of p by terminal words. The respective matching problem, i.e., deciding whether or not a given pattern matches a given ... More
Theoretical Limitations of Self-Attention in Neural Sequence ModelsJun 16 2019Transformers are emerging as the new workhorse of NLP, showing great success across tasks. Unlike LSTMs, transformers process input sequences entirely through self-attention. Previous work has suggested that the computational capabilities of self-attention ... More
A Congruence-based Perspective on Automata Minimization AlgorithmsJun 14 2019Jun 27 2019In this work we use a framework of finite-state automata constructions based on equivalences over words to provide new insights on the relation between well-known methods for computing the minimal deterministic automaton of a language.
A Congruence-based Perspective on Automata Minimization AlgorithmsJun 14 2019In this work we use a framework of finite-state automata constructions based on equivalences over words to provide new insights on the relation between well-known methods for computing the minimal deterministic automaton of a language.
Opportunistic Synthesis in Reactive Games under Information AsymmetryJun 13 2019Reactive synthesis is a class of methods to construct a provably-correct control system, referred to as a robot, with respect to a temporal logic specification in the presence of a dynamic and uncontrollable environment. This is achieved by modeling the ... More
Two modes of recognition: algebra, coalgebra, and languagesJun 13 2019The aim of the paper is to build a connection between two approaches towards categorical language theory: the coalgebraic and algebraic language theory for monads. For a pair of monads modelling the branching and the linear type we defined regular maps ... More
Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent SystemsJun 12 2019Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all ... More
Consistency in Parametric Interval Probabilistic Timed AutomataJun 12 2019We propose a new abstract formalism for probabilistic timed systems, Parametric Interval Probabilistic Timed Automata, based on an extension of Parametric Timed Automata and Interval Markov Chains. In this context, we consider the consistency problem ... More
Cyber attacks with bounded sensor reading edits for partially-observed discrete event systemsJun 12 2019The problem of cyber attacks with bounded sensor reading edits for partially-observed discrete event systems is considered. An operator observes a plant through an observation mask that does not allow him to detect the occurrence of certain events (silent ... More
Action-Sensitive Phonological DependenciesJun 12 2019This paper defines a subregular class of functions called the tier-based synchronized strictly local (TSSL) functions. These functions are similar to the the tier-based input-output strictly local (TIOSL) functions, except that the locality condition ... More
Formalization of the Axiom of Choice and its Equivalent TheoremsJun 10 2019In this paper, we describe the formalization of the axiom of choice and several of its famous equivalent theorems in Morse-Kelley set theory. These theorems include Tukey's lemma, the Hausdorff maximal principle, the maximal principle, Zermelo's postulate, ... More
Borders, Palindrome Prefixes, and Square PrefixesJun 09 2019We show that the number of length-$n$ words over a $k$-letter alphabet having no even palindromic prefix is the same as the number of length-$n$ unbordered words, by constructing an explicit bijection between the two sets. A similar result holds for those ... More
LSTM Networks Can Perform Dynamic CountingJun 09 2019In this paper, we systematically assess the ability of standard recurrent networks to perform dynamic counting and to encode hierarchical representations. All the neural models in our experiments are designed to be small-sized networks both to prevent ... More
An Automaton Group with PSPACE-Complete Word ProblemJun 08 2019We construct an automaton group with a PSPACE-complete word problem, proving a conjecture due to Steinberg. Additionally, the constructed group has a provably more difficult, namely EXPSPACE-complete, compressed word problem. Our construction directly ... More
Quasi-automatic semigroupsJun 06 2019Jun 10 2019A quasi-automatic semigroup is defined by a finite set of generators, a rational (regular) set of representatives, such that if a is a generator or neutral, then the graph of right multiplication by a on the set of representatives is a rational relation. ... More
Dynamically Allocated Memory Verification in Object-Oriented Programs using PrologJun 06 2019A Prolog-based framework for fully automated verification currently under development for heap-based object-oriented data is introduced. Dynamically allocated issues are discussed, recent approaches and criteria are analysed. The architecture and its ... More
Sequential Neural Networks as AutomataJun 04 2019This work attempts to explain the types of computation that neural networks can perform by relating them to automata. We first define what it means for a real-time network with bounded precision to accept a language. A measure of network memory follows ... More
Sequential Neural Networks as AutomataJun 04 2019Jun 05 2019This work attempts to explain the types of computation that neural networks can perform by relating them to automata. We first define what it means for a real-time network with bounded precision to accept a language. A measure of network memory follows ... More
Quasi-automatic groups are asynchronously automaticJun 04 2019A quasi-automatic semigroup is a finitely generated semigroup with a rational set of representatives such that the graph of right multiplication by any generator is a rational relation. A asynchronously automatic semigroup is a quasi-automatic semigroup ... More
Characteristic Parameters and Special Trapezoidal WordsJun 04 2019Following earlier work by Aldo de Luca and others, we study trapezoidal words and their prefixes, with respect to their characteristic parameters $K$ and $R$ (length of shortest unrepeated suffix, and shortest length without right special factors, respectively), ... More
Separation and Renaming in Nominal SetsJun 03 2019Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary ... More
On Modelling the Avoidability of Patterns as CSPJun 03 2019Solving avoidability problems in the area of string combinatorics often requires, in an initial step, the construction, via a computer program, of a very long word that does not contain any word that matches a given pattern. It is well known that this ... More
Every nonnegative real number is an abelian critical exponentJun 03 2019The abelian critical exponent of an infinite word $w$ is defined as the maximum ratio between the exponent and the period of an abelian power occurring in $w$. It was shown by Fici et al. that the set of finite abelian critical exponents of Sturmian words ... More
Abstract Predicate Entailment over Points-To Heaplets is Syntax RecognitionJun 01 2019Abstract predicates are considered in this paper as abstraction technique for heap-separated configurations, and as genuine Prolog predicates which are translated straight into a corresponding formal language grammar used as validation scheme for intermediate ... More
Concurrency in Boolean networksMay 31 2019Boolean networks (BNs) are widely used to model the qualitative dynamics of biological systems. Besides the logical rules determining the evolution of each component with respect to the state of its regulators, the scheduling of component updates can ... More
Understanding and Extending Incremental Determinization for 2QBFMay 31 2019Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determinization as a set of inference rules to help understand the design space ... More
String-to-String Interpretations with Polynomial-Size OutputMay 30 2019String-to-string MSO interpretations are like Courcelle's MSO transductions, except that a single output position can be represented using a tuple of input positions instead of just a single input position. In particular, the output length is polynomial ... More
Distribution of Behaviour into Parallel Communicating SubsystemsMay 30 2019The process of decomposing a complex system into simpler subsystems has been of interest to computer scientists over many decades, most recently for the field of distributed computing. In this paper, motivated by the desire to distribute the process of ... More
A Non-repetitive Logic for Verification of Dynamic Memory with Explicit Heap Conjunction and DisjunctionMay 30 2019In this paper, we review existing points-to Separation Logics for dynamic memory reasoning and we find that different usages of heap separation tend to be an obstacle. Hence, two total and strict spatial heap operations are proposed upon heap graphs, ... More
On multiplicative automatic sequencesMay 28 2019We show that any automatic multiplicative sequence either coincides with a Dirichlet character or is identically zero when restricted to integers not divisible by small primes. This answers a question of Bell, Bruin and Coons. A similar result was obtained ... More
New Results on Vector and Homing Vector AutomataMay 28 2019We present several new results and connections between various extensions of finite automata through the study of vector automata and homing vector automata. We show that homing vector automata outperform extended finite automata when both are defined ... More
On Collapsing Prefix Normal WordsMay 28 2019Prefix normal words are binary words in which each prefix has at least the same number of $\so$s as any factor of the same length. Firstly introduced by Fici and Lipt\'ak in 2011, the problem of determining the index of the prefix equivalence relation ... More
On the Containment Problem for Unambiguous Single-Register Automata with GuessingMay 28 2019Register automata extend classical finite automata with a finite set of registers that can store data from an infinite data domain for later equality comparisons with data from an input data word. While the registers in the original model of register ... More
On Timed Scope-bounded Context-sensitive LanguagesMay 27 2019In (DLT 2016) we studied timed context sensitive languages characterized by multiple stack push down automata (MPA), with an explicit bound on number of stages where in each stage at most one stack is used (k-round MPA). In this paper, we continue our ... More
Recognizing pro-R closures of regular languagesMay 24 2019Given a regular language L, we effectively construct a unary semigroup that recognizes the topological closure of L in the free unary semigroup relative to the variety of unary semigroups generated by the pseudovariety R of all finite R-trivial semigroups. ... More
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)May 24 2019We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines ... More
Formalizing Time4sys using parametric timed automataMay 23 2019Critical real-time systems must be verified to avoid the risk of dramatic consequences in case of failure. Thales developed an open formalism Time4sys to model real-time systems, with expressive features such as periodic or sporadic tasks, task dependencies, ... More
Sampling from Stochastic Finite Automata with Applications to CTC DecodingMay 21 2019Stochastic finite automata arise naturally in many language and speech processing tasks. They include stochastic acceptors, which represent certain probability distributions over random strings. We consider the problem of efficient sampling: drawing random ... More
Approximating probabilistic models as weighted finite automataMay 21 2019Weighted finite automata (WFA) are often used to represent probabilistic models, such as $n$-gram language models, since they are efficient for recognition tasks in time and space. The probabilistic source to be represented as a WFA, however, may come ... More
Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)May 21 2019We propose a lazy decision procedure for the logic WSkS. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical WSkS decision procedure. The classical decision procedure transforms the ... More
Behavioural Preorders on Stochastic Systems - Logical, Topological, and Computational AspectsMay 21 2019Computer systems can be found everywhere: in space, in our homes, in our cars, in our pockets, and sometimes even in our own bodies. For concerns of safety, economy, and convenience, it is important that such systems work correctly. However, it is a notoriously ... More
ATAC: A Tool for Automating Timed Automata ConstructionMay 20 2019In this paper, we focus on the design of timed automata (TA) and introduce a new tool for automating TA construction. Our tool generates TA models from descriptions and specifications given in structured natural language. We define a sufficient set of ... More
A combinatorial approach for the state complexity of the Shuffle productMay 20 2019We investigate the state complexity of the shuffle operation on regular languages initiated by Campeanu et al. and studied subsequently by Brzozowski et al. We shift the problem into the combinatorics domain by turning the problem of state accessibility ... More
The teaching complexity of erasing pattern languages with bounded variable frequencyMay 19 2019Patterns provide a concise, syntactic way of describing a set of strings, but their expressive power comes at a price: a number of fundamental decision problems concerning (erasing) pattern languages, such as the membership problem and inclusion problem, ... More
Abstraction Refinement Algorithms for Timed AutomataMay 17 2019May 20 2019We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement ... More
Abstraction Refinement Algorithms for Timed AutomataMay 17 2019May 24 2019We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement ... More
Abstraction Refinement Algorithms for Timed AutomataMay 17 2019We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement ... More
Separating many words by counting occurrences of factorsMay 17 2019For a given language $L$, we study the languages $X$ such that for all distinct words $u, v \in L$, there exists a word $x \in X$ that appears a different number of times as a factor in $u$ and in $v$. In particular, we are interested in the following ... More
Simulations in Rank-Based Büchi Automata ComplementationMay 17 2019The long search for an optimal complementation construction for B\"uchi automata climaxed with the work of Schewe, who proposed a worst-case optimal rank-based procedure that generates complements of a size matching the theoretical lower bound of (0.76n)n, ... More
Making Agile Development Processes fit for V-style Certification ProceduresMay 16 2019We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an "agile development" ... More
Abelian periods of factors of Sturmian wordsMay 15 2019We study the abelian period sets of Sturmian words, which are codings of irrational rotations on a one-dimensional torus. The main result states that the minimum abelian period of a factor of a Sturmian word of angle $\alpha$ with continued fraction expansion ... More
Deciding the Computability of Regular Functions over Infinite WordsMay 15 2019The class of regular functions from infinite words to infinite words is characterised by MSO-transducers, streaming $\omega$-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers ... More
Long-Run Average Behavior of Vector Addition Systems with StatesMay 14 2019A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While ... More
A (co)algebraic theory of succinct automataMay 14 2019The classical subset construction for non-deterministic automata can be generalized to other side-effects captured by a monad. The key insight is that both the state space of the determinized automaton and its semantics---languages over an alphabet---have ... More
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTPMay 14 2019The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified ... More
On Semigroups of Two-Dimensional Upper-Triangular Integer MatricesMay 13 2019We analyze algorithmic problems in finitely generated semigroups of two-dimensional upper-triangular integer matrices. These semigroup problems are tightly connected with problems about compositions of affine functions over one variable. Building on a ... More
Symbolic Monitoring against Specifications Parametric in Time and DataMay 11 2019Monitoring consists in deciding whether a log meets a given specification. In this work, we propose an automata-based formalism to monitor logs in the form of actions associated with time stamps and arbitrarily data values over infinite domains. Our formalism ... More
The Complexity of Transducer Synthesis from Multi-Sequential SpecificationsMay 09 2019The transducer synthesis problem on finite words asks, given a specification $S \subseteq I \times O$, where $I$ and $O$ are sets of finite words, whether there exists an implementation $f: I \rightarrow O$ which (1) fulfils the specification, i.e., $(i,f(i))\in ... More
Synthesis of Data Word TransducersMay 09 2019In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite ... More