arXiv subjects

Vrunda Dave

Publications and source records attributed to Vrunda Dave.

5 recordsLinked to original sources

arXiv2022

Optimal Repair For Omega-regular Properties

This paper presents an optimization based framework to automate system repair against omega-regular properties. In the proposed formalization of optimal repair, the systems are represented as Kripke structures, the properties as $ω$-regular languages, and the repair space as repair machines -- weighted omega-regular transducers equipped with Büchi conditions -- that rewrite strings and associate a cost sequence to these rewritings. To translate the resulting cost-sequences to easily interpretable payoffs, we consider several aggregator functions to map cost sequences to numbers -- including limit superior, supremum, discounted-sum, and average-sum -- to define quantitative cost semantics. The problem of optimal repair, then, is to determine whether traces from a given system can be rewritten to satisfy an $ω$-regular property when the allowed cost is bounded by a given threshold. We also consider the dual challenge of impair verification that assumes that the rewritings are resolved adversarially under some given cost restriction, and asks to decide if all traces of the system satisfy the specification irrespective of the rewritings. With a negative result to the impair verification problem, we study the problem of designing a minimal mask of the Kripke structure such that the resulting traces satisfy the specifications despite the threshold-bounded impairment. We dub this problem as the mask synthesis problem. This paper presents automata-theoretic solutions to repair synthesis, impair verification, and mask synthesis problem for limit superior, supremum, discounted-sum, and average-sum cost semantics.

cs.FL↗

arXiv2021

Regular Model Checking with Regular Relations

Regular model checking is an exploration technique for infinite state systems where state spaces are represented as regular languages and transition relations are expressed using rational relations over infinite (or finite) strings. We extend the regular model checking paradigm to permit the use of more powerful transition relations: the class of regular relations, of which the rational relations are a strict subset. We use the language of monadic second-order logic on infinite strings to specify such relations and adopt streaming string transducers (SSTs) as a suitable computational model. We introduce nondeterministic SSTs over infinite strings and show that they precisely capture the relations definable in MSO. We further explore theoretical properties of omega-NSSTs required to effectively carry out regular model checking. In particular, we establish that the regular type checking problem for omega-NSSTs is decidable in PSPACE. Since the post-image of a regular language under a regular relation may not be regular (or even context-free), approaches that iteratively compute the image can not be effectively carried out in this setting. Instead, we utilize the fact that regular relations are closed under composition, which, together with our decidability result, provides a foundation for regular model checking with regular relations.

cs.LO↗

arXiv2020

On the Separability Problem of String Constraints

We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an EXPSPACE algorithm for the separability of a useful class of straight-line string constraints, and a PSPACE-hardness result.

cs.FL↗

arXiv2018

Regular Transducer Expressions for Regular Transformations

Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). For infinite words, the transducer uses Muller acceptance and $ω$-regular look-ahead. \RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al.\ in LICS'14. In order to construct an RTE associated with a deterministic two-way Muller transducer with look-ahead, we introduce the notion of transition monoid for such two-way transducers where the look-ahead is captured by some backward deterministic Büchi automaton. Then, we use an unambiguous version of Imre Simon's famous forest factorization theorem in order to derive a "good" ($ω$-)regular expression for the domain of the two-way transducer. "Good" expressions are unambiguous and Kleene-plus as well as $ω$-iterations are only used on subexpressions corresponding to \emph{idempotent} elements of the transition monoid. The combinator expressions are finally constructed by structural induction on the "good" ($ω$-)regular expression describing the domain of the transducer.

cs.FL↗

arXiv2016

FO-definable transformations of infinite strings

The theory of regular and aperiodic transformations of finite strings has recently received a lot of interest. These classes can be equivalently defined using logic (Monadic second-order logic and first-order logic), two-way machines (regular two-way and aperiodic two-way transducers), and one-way register machines (regular streaming string and aperiodic streaming string transducers). These classes are known to be closed under operations such as sequential composition and regular (star-free) choice; and problems such as functional equivalence and type checking, are decidable for these classes. On the other hand, for infinite strings these results are only known for $ω$-regular transformations: Alur, Filiot, and Trivedi studied transformations of infinite strings and introduced an extension of streaming string transducers over $ω$-strings and showed that they capture monadic second-order definable transformations for infinite strings. In this paper we extend their work to recover connection for infinite strings among first-order logic definable transformations, aperiodic two-way transducers, and aperiodic streaming string transducers.

cs.FL↗