-
Deterministic Weighted Automata under Partial Observability
Authors:
Jakub Michaliszyn,
Jan Otop
Abstract:
Weighted automata is a basic tool for specification in quantitative verification, which allows to express quantitative features of analysed systems such as resource consumption. Quantitative specification can be assisted by automata learning as there are classic results on Angluin-style learning of weighted automata. The existing work assumes perfect information about the values returned by the ta…
▽ More
Weighted automata is a basic tool for specification in quantitative verification, which allows to express quantitative features of analysed systems such as resource consumption. Quantitative specification can be assisted by automata learning as there are classic results on Angluin-style learning of weighted automata. The existing work assumes perfect information about the values returned by the target weighted automaton. In assisted synthesis of a quantitative specification, knowledge of the exact values is a strong assumption and may be infeasible. In our work, we address this issue by introducing a new framework of partially-observable deterministic weighted automata, in which weighted automata return intervals containing the computed values of words instead of the exact values. We study the basic properties of this framework with the particular focus on the challenges of
△ Less
Submitted 1 March, 2024;
originally announced March 2024.
-
Multi-dimensional Long-Run Average Problems for Vector Addition Systems with States
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Jan Otop
Abstract:
A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A prob…
▽ More
A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.
△ Less
Submitted 17 July, 2020;
originally announced July 2020.
-
Modular Path Queries with Arithmetic
Authors:
Jakub Michaliszyn,
Jan Otop,
Piotr Wieczorek
Abstract:
We propose a new approach to querying graph databases. Our approach balances competing goals of expressive power, language clarity and computational complexity. A distinctive feature of our approach is the ability to express properties of minimal (e.g. shortest) and maximal (e.g. most valuable) paths satisfying given criteria. To express complex properties in a modular way, we introduce labelling-…
▽ More
We propose a new approach to querying graph databases. Our approach balances competing goals of expressive power, language clarity and computational complexity. A distinctive feature of our approach is the ability to express properties of minimal (e.g. shortest) and maximal (e.g. most valuable) paths satisfying given criteria. To express complex properties in a modular way, we introduce labelling-generating ontologies. The resulting formalism is computationally attractive - queries can be answered in non-deterministic logarithmic space in the size of the database.
△ Less
Submitted 17 September, 2021; v1 submitted 11 February, 2020;
originally announced February 2020.
-
Non-deterministic weighted automata evaluated over Markov chains
Authors:
Jakub Michaliszyn,
Jan Otop
Abstract:
We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables.
The exact answers to the probabi…
▽ More
We present the first study of non-deterministic weighted automata under probabilistic semantics. In this semantics words are random events, generated by a Markov chain, and functions computed by weighted automata are random variables. We consider the probabilistic questions of computing the expected value and the cumulative distribution for such random variables.
The exact answers to the probabilistic questions for non-deterministic automata can be irrational and are uncomputable in general. To overcome this limitation, we propose approximation algorithms for the probabilistic questions, which work in exponential time in the size of the automaton and polynomial time in the size of the Markov chain and the given precision. We apply this result to show that non-deterministic automata can be effectively determinised with respect to the standard deviation metric.
△ Less
Submitted 31 October, 2019; v1 submitted 13 August, 2019;
originally announced August 2019.
-
Approximate Learning of Limit-Average Automata
Authors:
Jakub Michaliszyn,
Jan Otop
Abstract:
Limit-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 case, we show that limit-average automata are not PAC-learnable as samples must be of exponential-size to provide (with good probability) enough…
▽ More
Limit-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 case, we show that limit-average automata are not PAC-learnable as samples must be of exponential-size to provide (with good probability) enough details to learn an automaton. We also show that the problem of finding an automaton that fits a given sample is NP-complete. In the active learning case, we show that limit-average automata can be learned almost-exactly, i.e., we can learn in polynomial time an automaton that is consistent with the target automaton on almost all words. On the other hand, we show that the problem of learning an automaton that approximates the target automaton (with perhaps fewer states) is NP-complete. The abovementioned results are shown for the uniform distribution on words. We briefly discuss learning over different distributions.
△ Less
Submitted 26 June, 2019;
originally announced June 2019.
-
Long-Run Average Behavior of Vector Addition Systems with States
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Jan Otop
Abstract:
A 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 qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite co…
▽ More
A 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 qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a)~decidable in polynomial time for integer-valued VASS, and (b)~decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c)~NP-complete for integer-valued VASS, and (d)~undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.
△ Less
Submitted 14 May, 2019;
originally announced May 2019.
-
Average Stack Cost of Buechi Pushdown Automata
Authors:
Jakub Michaliszyn,
Jan Otop
Abstract:
We study the average stack cost of Buechi pushdown automata (Buechi PDA). We associate a non-negative price with each stack symbol and define the cost of a stack as the sum of costs of all its elements. We introduce and study the average stack cost problem (ASC), which asks whether there exists an accepting run of a given Buechi PDA such that the long-run average of stack costs is below some given…
▽ More
We study the average stack cost of Buechi pushdown automata (Buechi PDA). We associate a non-negative price with each stack symbol and define the cost of a stack as the sum of costs of all its elements. We introduce and study the average stack cost problem (ASC), which asks whether there exists an accepting run of a given Buechi PDA such that the long-run average of stack costs is below some given threshold. The ASC problem generalizes mean-payoff objective and can be used to express quantitative properties of pushdown systems. In particular, we can compute the average response time using the ASC problem. We show that the ASC problem can be solved in polynomial time.
△ Less
Submitted 12 October, 2017;
originally announced October 2017.
-
Querying Best Paths in Graph Databases
Authors:
Jakub Michaliszyn,
Jan Otop,
Piotr Wieczorek
Abstract:
Querying graph databases has recently received much attention. We propose a new approach to this problem, which balances competing goals of expressive power, language clarity and computational complexity. A distinctive feature of our approach is the ability to express properties of minimal (e.g. shortest) and maximal (e.g. most valuable) paths satisfying given criteria. To express complex properti…
▽ More
Querying graph databases has recently received much attention. We propose a new approach to this problem, which balances competing goals of expressive power, language clarity and computational complexity. A distinctive feature of our approach is the ability to express properties of minimal (e.g. shortest) and maximal (e.g. most valuable) paths satisfying given criteria. To express complex properties in a modular way, we introduce labelling-generating ontologies. The resulting formalism is computationally attractive -- queries can be answered in non-deterministic logarithmic space in the size of the database.
△ Less
Submitted 12 October, 2017;
originally announced October 2017.
-
Bidirectional Nested Weighted Automata
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Jan Otop
Abstract:
Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We the…
▽ More
Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.
△ Less
Submitted 26 June, 2017;
originally announced June 2017.
-
Nested Weighted Limit-Average Automata of Bounded Width
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Jan Otop
Abstract:
While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weight…
▽ More
While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlap** requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.
△ Less
Submitted 11 June, 2016;
originally announced June 2016.
-
Quantitative Automata under Probabilistic Semantics
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Jan Otop
Abstract:
Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative autom…
▽ More
Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider.
△ Less
Submitted 10 August, 2019; v1 submitted 22 April, 2016;
originally announced April 2016.
-
Lipschitz Robustness of Timed I/O Systems
Authors:
Thomas A. Henzinger,
Jan Otop,
Roopsha Samanta
Abstract:
We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of "uncertain inputs" and formalize their robustness using the analytic notion of Lipschitz continuity. Thus, a timed I/O system is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input.…
▽ More
We present the first study of robustness of systems that are both timed as well as reactive (I/O). We study the behavior of such timed I/O systems in the presence of "uncertain inputs" and formalize their robustness using the analytic notion of Lipschitz continuity. Thus, a timed I/O system is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using "similarity functions" over timed words such as the timed version of the Manhattan distance and the Skorokhod distance. We consider two models of timed I/O systems --- timed transducers and asynchronous sequential circuits. While K-robustness is undecidable even for discrete transducers, we identify a class of timed transducers which admits a polynomial space decision procedure for K-robustness. For asynchronous sequential circuits, we reduce K-robustness w.r.t. timed Manhattan distances to K-robusness of discrete letter-to-letter transducers and show PSPACE-compeleteness of the problem.
△ Less
Submitted 3 June, 2015;
originally announced June 2015.
-
Edit Distance for Pushdown Automata
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Rasmus Ibsen-Jensen,
Jan Otop
Abstract:
The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to $\mathcal{L}_2$ is the minimal number $k$ such that for every word from $\mathcal{L}_1$ there exists…
▽ More
The edit distance between two words $w_1, w_2$ is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform $w_1$ to $w_2$. The edit distance generalizes to languages $\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to $\mathcal{L}_2$ is the minimal number $k$ such that for every word from $\mathcal{L}_1$ there exists a word in $\mathcal{L}_2$ with edit distance at most $k$. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1)~deciding whether, for a given threshold $k$, the edit distance from a pushdown automaton to a finite automaton is at most $k$, and (2)~deciding whether the edit distance from a pushdown automaton to a finite automaton is finite.
△ Less
Submitted 22 September, 2017; v1 submitted 30 April, 2015;
originally announced April 2015.
-
Nested Weighted Automata
Authors:
Krishnendu Chatterjee,
Thomas A. Henzinger,
Jan Otop
Abstract:
Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know dec…
▽ More
Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.
△ Less
Submitted 23 April, 2015;
originally announced April 2015.
-
Lipschitz Robustness of Finite-state Transducers
Authors:
Thomas A. Henzinger,
Jan Otop,
Roopsha Samanta
Abstract:
We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity --- a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-ro…
▽ More
We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity --- a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using set-similarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers.
△ Less
Submitted 7 October, 2014; v1 submitted 25 April, 2014;
originally announced April 2014.
-
Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
Authors:
Jakub Michaliszyn,
Jan Otop,
Piotr Witkowski
Abstract:
We study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for f…
▽ More
We study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for finite satisfiability [11, 12, 16, 17]. In this paper, we show that there is a reason why we must deal with both kinds of satisfiability separately -- we prove that there is a universal first-order formula that defines an elementary modal logic with decidable (global) satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.
△ Less
Submitted 8 October, 2012;
originally announced October 2012.
