Showing 1–21 of 21 results for author: Fisman, D

A Robust Measure on FDFAs Following Duo-Normalized Acceptance

Authors: Dana Fisman, Emmanuel Goldberg, Oded Zimerman

Abstract: Families of DFAs (FDFAs) are a computational model recognizing $ω$-regular languages. They were introduced in the quest of finding a Myhill-Nerode theorem for $ω$-regular languages, and obtaining learning algorithms. FDFAs have been shown to have good qualities in terms of the resources required for computing Boolean operations on them (complementation, union, and intersection) and answering decis… ▽ More Families of DFAs (FDFAs) are a computational model recognizing $ω$-regular languages. They were introduced in the quest of finding a Myhill-Nerode theorem for $ω$-regular languages, and obtaining learning algorithms. FDFAs have been shown to have good qualities in terms of the resources required for computing Boolean operations on them (complementation, union, and intersection) and answering decision problems (emptiness and equivalence); all can be done in non-deterministic logspace. In this paper we study FDFAs with a new type of acceptance condition, duo-normalization, that generalizes the traditional normalization acceptance type. We show that duo-normalized FDFAs are advantageous to normalized FDFAs in terms of succinctness as they can be exponentially smaller. Fortunately this added succinctness doesn't come at the cost of increasing the complexity of Boolean operations and decision problems -- they can still be preformed in non-deterministic logspace. An important measure of the complexity of an $ω$-regular language, is its position in the Wagner hierarchy. It is based on the inclusion measure of Muller automata and for the common $ω$-automata there exist algorithms computing their position. We develop a similarly robust measure for duo-normalized (and normalized) FDFAs, which we term the diameter measure. We show that the diameter measure corresponds one-to-one to the position on the Wagner hierarchy. We show that computing it for duo-normalized FDFAs is PSPACE-complete, while it can be done in non-deterministic logspace for traditional FDFAs. △ Less

Submitted 21 February, 2024; v1 submitted 24 October, 2023; originally announced October 2023.

ACM Class: F.4.3

Learning Broadcast Protocols

Authors: Dana Fisman, Noa Izsak, Swen Jacobs

Abstract: The problem of learning a computational model from examples has been receiving growing attention. For the particularly challenging problem of learning models of distributed systems, existing results are restricted to models with a fixed number of interacting processes. In this work we look for the first time (to the best of our knowledge) at the problem of learning a distributed system with an arb… ▽ More The problem of learning a computational model from examples has been receiving growing attention. For the particularly challenging problem of learning models of distributed systems, existing results are restricted to models with a fixed number of interacting processes. In this work we look for the first time (to the best of our knowledge) at the problem of learning a distributed system with an arbitrary number of processes, assuming only that there exists a cutoff, i.e., a number of processes that is sufficient to produce all observable behaviors. Specifically, we consider fine broadcast protocols, these are broadcast protocols (BPs) with a finite cutoff and no hidden states. We provide a learning algorithm that can infer a correct BP from a sample that is consistent with a fine BP, and a minimal equivalent BP if the sample is sufficiently complete. On the negative side we show that (a) characteristic sets of exponential size are unavoidable, (b) the consistency problem for fine BPs is NP hard, and (c) that fine BPs are not polynomially predictable. △ Less

Submitted 11 December, 2023; v1 submitted 25 June, 2023; originally announced June 2023.

Comments: 13 pages, 7 figures, 3 input files of plots

ACM Class: F.4.3

Constructing Concise Characteristic Samples for Acceptors of Omega Regular Languages

Authors: Dana Angluin, Dana Fisman

Abstract: A characteristic sample for a language $L$ and a learning algorithm $\textbf{L}$ is a finite sample of words $T_L$ labeled by their membership in $L$ such that for any sample $T \supseteq T_L$ consistent with $L$, on input $T$ the learning algorithm $\textbf{L}$ returns a hypothesis equivalent to $L$. Which omega automata have characteristic sets of polynomial size, and can these sets be construct… ▽ More A characteristic sample for a language $L$ and a learning algorithm $\textbf{L}$ is a finite sample of words $T_L$ labeled by their membership in $L$ such that for any sample $T \supseteq T_L$ consistent with $L$, on input $T$ the learning algorithm $\textbf{L}$ returns a hypothesis equivalent to $L$. Which omega automata have characteristic sets of polynomial size, and can these sets be constructed in polynomial time? We address these questions here. In brief, non-deterministic omega automata of any of the common types, in particular Büchi, do not have characteristic samples of polynomial size. For deterministic omega automata that are isomorphic to their right congruence automata, the fully informative languages, polynomial time algorithms for constructing characteristic samples and learning from them are given. The algorithms for constructing characteristic sets in polynomial time for the different omega automata (of types Büchi, coBüchi, parity, Rabin, Street, or Muller), require deterministic polynomial time algorithms for (1) equivalence of the respective omega automata, and (2) testing membership of the language of the automaton in the informative classes, which we provide. △ Less

Submitted 22 April, 2024; v1 submitted 19 September, 2022; originally announced September 2022.

ACM Class: F.4.3

Learning of Structurally Unambiguous Probabilistic Grammars

Authors: Dana Fisman, Dolav Nitay, Michal Ziv-Ukelson

Abstract: The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness results for learning context-free grammars in general, and probabilistic grammars in particular, most of the literature has concentrated on the second problem.… ▽ More The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness results for learning context-free grammars in general, and probabilistic grammars in particular, most of the literature has concentrated on the second problem. In this work we address the first problem. We restrict attention to structurally unambiguous weighted context-free grammars (SUWCFG) and provide a query learning algorithm for \structurally unambiguous probabilistic context-free grammars (SUPCFG). We show that SUWCFG can be represented using \emph{co-linear multiplicity tree automata} (CMTA), and provide a polynomial learning algorithm that learns CMTAs. We show that the learned CMTA can be converted into a probabilistic grammar, thus providing a complete algorithm for learning a structurally unambiguous probabilistic context free grammar (both the grammar topology and the probabilistic weights) using structured membership queries and structured equivalence queries. A summarized version of this work was published at AAAI 21. △ Less

Submitted 7 February, 2023; v1 submitted 17 March, 2022; originally announced March 2022.

Comments: arXiv admin note: substantial text overlap with arXiv:2011.07472

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 1 (February 8, 2023) lmcs:9223

The Normalized Edit Distance with Uniform Operation Costs is a Metric

Authors: Dana Fisman, Joshua Grogin, Oded Margalit, Gera Weiss

Abstract: We prove that the normalized edit distance proposed in [Marzal and Vidal 1993] is a metric when the cost of all the edit operations are the same. This closes a long standing gap in the literature where several authors noted that this distance does not satisfy the triangle inequality in the general case, and that it was not known whether it is satisfied in the uniform case where all the edit costs… ▽ More We prove that the normalized edit distance proposed in [Marzal and Vidal 1993] is a metric when the cost of all the edit operations are the same. This closes a long standing gap in the literature where several authors noted that this distance does not satisfy the triangle inequality in the general case, and that it was not known whether it is satisfied in the uniform case where all the edit costs are equal. We compare this metric to two normalized metrics proposed as alternatives in the literature, when people thought that Marzal's and Vidal's distance is not a metric, and identify key properties that explain why the original distance, now known to also be a metric, is better for some applications. Our examination is from a point of view of formal verification, but the properties and their significance are stated in an application agnostic way. △ Less

Submitted 23 April, 2022; v1 submitted 16 January, 2022; originally announced January 2022.

Comments: 14 pages, 0 figures, accepted to CPM 2022

Inferring Symbolic Automata

Authors: Dana Fisman, Hadar Frenkel, Sandra Zilles

Abstract: We study the learnability of symbolic finite state automata (SFA), a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all obtained results are positive. We provide a necessary condition for efficient learnability of SFAs in this paradigm, from which we obtain the first negative result. Th… ▽ More We study the learnability of symbolic finite state automata (SFA), a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all obtained results are positive. We provide a necessary condition for efficient learnability of SFAs in this paradigm, from which we obtain the first negative result. The main focus of our work lies in the learnability of SFAs under the paradigm of identification in the limit using polynomial time and data, and its strengthening efficient identifiability, which are concerned with the existence of a systematic set of characteristic samples from which a learner can correctly infer the target language. We provide a necessary condition for identification of SFAs in the limit using polynomial time and data, and a sufficient condition for efficient learnability of SFAs. From these conditions we derive a positive and a negative result. The performance of a learning algorithm is typically bounded as a function of the size of the representation of the target language. Since SFAs, in general, do not have a canonical form, and there are trade-offs between the complexity of the predicates on the transitions and the number of transitions, we start by defining size measures for SFAs. We revisit the complexity of procedures on SFAs and analyze them according to these measures, paying attention to the special forms of SFAs: normalized SFAs and neat SFAs, as well as to SFAs over a monotonic effective Boolean algebra. This is an extended version of the paper with the same title published in CSL'22. △ Less

Submitted 19 April, 2023; v1 submitted 28 December, 2021; originally announced December 2021.

Comments: arXiv admin note: text overlap with arXiv:2011.05389

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 2 (April 20, 2023) lmcs:8899

Safety Synthesis Sans Specification

Authors: Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Dana Fisman, Heinz Riener

Abstract: We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that… ▽ More We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation. △ Less

Submitted 27 November, 2020; v1 submitted 15 November, 2020; originally announced November 2020.

Learning of Structurally Unambiguous Probabilistic Grammars

Authors: Dolav Nitay, Dana Fisman, Michal Ziv-Ukelson

Abstract: The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness results for learning context-free grammars in general, and probabilistic grammars in particular, most of the literature has concentrated on the second problem.… ▽ More The problem of identifying a probabilistic context free grammar has two aspects: the first is determining the grammar's topology (the rules of the grammar) and the second is estimating probabilistic weights for each rule. Given the hardness results for learning context-free grammars in general, and probabilistic grammars in particular, most of the literature has concentrated on the second problem. In this work we address the first problem. We restrict attention to structurally unambiguous weighted context-free grammars (SUWCFG) and provide a query learning algorithm for structurally unambiguous probabilistic context-free grammars (SUPCFG). We show that SUWCFG can be represented using co-linear multiplicity tree automata (CMTA), and provide a polynomial learning algorithm that learns CMTAs. We show that the learned CMTA can be converted into a probabilistic grammar, thus providing a complete algorithm for learning a structurally unambiguous probabilistic context free grammar (both the grammar topology and the probabilistic weights) using structured membership queries and structured equivalence queries. We demonstrate the usefulness of our algorithm in learning PCFGs over genomic data. △ Less

Submitted 9 March, 2021; v1 submitted 15 November, 2020; originally announced November 2020.

On the Complexity of Symbolic Finite-State Automata

Authors: Dana Fisman, Hadar Frenkel, Sandra Zilles

Abstract: We revisit the complexity of procedures on SFAs (such as intersection, emptiness, etc.) and analyze them according to the measures we find suitable for symbolic automata: the number of states, the maximal number of transitions exiting a state, and the size of the most complex transition predicate. We pay attention to the special forms of SFAs: {normalized SFAs} and {neat SFAs}, as well as to SFAs… ▽ More We revisit the complexity of procedures on SFAs (such as intersection, emptiness, etc.) and analyze them according to the measures we find suitable for symbolic automata: the number of states, the maximal number of transitions exiting a state, and the size of the most complex transition predicate. We pay attention to the special forms of SFAs: {normalized SFAs} and {neat SFAs}, as well as to SFAs over a {monotonic} effective Boolean algebra. △ Less

Submitted 2 July, 2021; v1 submitted 10 November, 2020; originally announced November 2020.

Learning Interpretable Models in the Property Specification Language

Authors: Rajarshi Roy, Dana Fisman, Daniel Neider

Abstract: We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of the recent work in this area, which focuses on descriptions expressed in Linear Temporal Logic (LTL), we develop a learning algorithm for formulas in the IEEE standard temporal logic PSL (Property Specification Language)… ▽ More We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of the recent work in this area, which focuses on descriptions expressed in Linear Temporal Logic (LTL), we develop a learning algorithm for formulas in the IEEE standard temporal logic PSL (Property Specification Language). Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in LTL, whereas it is easy to express such properties in PSL. Moreover, formulas in PSL can be more succinct and easier to interpret (due to the use of regular expressions in PSL formulas) than formulas in LTL. Our learning algorithm builds on top of an existing algorithm for learning LTL formulas. Roughly speaking, our algorithm reduces the learning task to a constraint satisfaction problem in propositional logic and then uses a SAT solver to search for a solution in an incremental fashion. We have implemented our algorithm and performed a comparative study between the proposed method and the existing LTL learning algorithm. Our results illustrate the effectiveness of the proposed approach to provide succinct human-interpretable descriptions from examples. △ Less

Submitted 10 February, 2020; originally announced February 2020.

Polynomial time algorithms for inclusion and equivalence of deterministic omega acceptors

Authors: Dana Angluin, Dana Fisman

Abstract: The class of omega languages recognized by deterministic parity acceptors (DPAs) or deterministic Muller acceptors (DMAs) is exactly the regular omega languages. The inclusion problem is the following: given two acceptors A1 and A2, determine whether the language recognized by A1 is a subset of the language recognized by A2, and if not, return an ultimately periodic omega word accepted by A1 but n… ▽ More The class of omega languages recognized by deterministic parity acceptors (DPAs) or deterministic Muller acceptors (DMAs) is exactly the regular omega languages. The inclusion problem is the following: given two acceptors A1 and A2, determine whether the language recognized by A1 is a subset of the language recognized by A2, and if not, return an ultimately periodic omega word accepted by A1 but not A2. We describe polynomial time algorithms to solve this problem for two DPAs and for two DMAs. Corollaries include polynomial time algorithms to solve the equivalence problem for DPAs and DMAs, and also the inclusion and equivalence problems for deterministic Buechi and coBuechi acceptors. △ Less

Submitted 9 May, 2020; v1 submitted 8 February, 2020; originally announced February 2020.

ACM Class: F.4.3

SyGuS-Comp 2018: Results and Analysis

Authors: Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, Abhishek Udupa

Abstract: Syntax-guided synthesis (SyGuS) is the computational problem of finding an implementation $f$ that meets both a semantic constraint given by a logical formula $φ$ in a background theory $\mathbb{T}$, and a syntactic constraint given by a grammar $G$, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in the SyGuS input format (SyGuS-IF),… ▽ More Syntax-guided synthesis (SyGuS) is the computational problem of finding an implementation $f$ that meets both a semantic constraint given by a logical formula $φ$ in a background theory $\mathbb{T}$, and a syntactic constraint given by a grammar $G$, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in the SyGuS input format (SyGuS-IF), a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In the 5th SyGuS-Comp, five solvers competed on over 1600 benchmarks across various tracks. This paper presents and analyses the results of this year's (2018) SyGuS competition. △ Less

Submitted 12 April, 2019; originally announced April 2019.

Comments: 18 pages. Satellite event of CAV'18 and SYNT'18. arXiv admin note: substantial text overlap with arXiv:1711.11438

Regular omega-Languages with an Informative Right Congruence

Authors: Dana Angluin, Dana Fisman

Abstract: A regular language is almost fully characterized by its right congruence relation. Indeed, a regular language can always be recognized by a DFA isomorphic to the automaton corresponding to its right congruence, henceforth the Rightcon automaton. The same does not hold for regular omega-languages. The right congruence of a regular omega-language is not informative enough; many regular omega-langua… ▽ More A regular language is almost fully characterized by its right congruence relation. Indeed, a regular language can always be recognized by a DFA isomorphic to the automaton corresponding to its right congruence, henceforth the Rightcon automaton. The same does not hold for regular omega-languages. The right congruence of a regular omega-language is not informative enough; many regular omega-languages have a trivial right congruence, and in general it is not always possible to define an omega-automaton recognizing a given language that is isomorphic to the rightcon automaton. The class of weak regular omega-languages does have an informative right congruence. That is, any weak regular omega-language can always be recognized by a deterministic Büchi automaton that is isomorphic to the rightcon automaton. Weak regular omega-languages reside in the lower levels of the expressiveness hierarchy of regular omega-languages. Are there more expressive sub-classes of regular omega languages that have an informative right congruence? Can we fully characterize the class of languages with a trivial right congruence? In this paper we try to place some additional pieces of this big puzzle. △ Less

Submitted 9 September, 2018; originally announced September 2018.

Comments: In Proceedings GandALF 2018, arXiv:1809.02416

Journal ref: EPTCS 277, 2018, pp. 265-279

Streamable Regular Transductions

Authors: Rajeev Alur, Dana Fisman, Konstantinos Mamouras, Mukund Raghothaman, Caleb Stanford

Abstract: Motivated by real-time monitoring and data processing applications, we develop a formal theory of quantitative queries for streaming data that can be evaluated efficiently. We consider the model of unambiguous Cost Register Automata (CRAs), which are machines that combine finite-state control (for identifying regular patterns) with a finite set of data registers (for computing numerical aggregates… ▽ More Motivated by real-time monitoring and data processing applications, we develop a formal theory of quantitative queries for streaming data that can be evaluated efficiently. We consider the model of unambiguous Cost Register Automata (CRAs), which are machines that combine finite-state control (for identifying regular patterns) with a finite set of data registers (for computing numerical aggregates). The definition of CRAs is parameterized by the collection of numerical operations that can be applied to the registers. These machines give rise to the class of streamable regular transductions (SR), and to the class of streamable linear regular transductions (SLR) when the register updates are copyless, i.e. every register appears at most once the right-hand-side expressions of the updates. We give a logical characterization of the class SR (resp., SLR) using MSO-definable transformations from strings to DAGs (resp., trees) without backward edges. Additionally, we establish that the two classes SR and SLR are closed under operations that are relevant for designing query languages. Finally, we study the relationship with weighted automata (WA), and show that CRAs over a suitably chosen set of operations correspond to WA, thus establishing that WA are a special case of CRAs. △ Less

Submitted 3 November, 2019; v1 submitted 10 July, 2018; originally announced July 2018.

Comments: 53 pages

Query learning of derived $ω$-tree languages in polynomial time

Authors: Dana Angluin, Timos Antonopoulos, Dana Fisman

Abstract: We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of $ω$-tree languages derived from weak regular $ω$-word languages in polynomial time. The method is a general polynomial time reduction of learning a class of derived $ω$-tree languages to learning the under… ▽ More We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of $ω$-tree languages derived from weak regular $ω$-word languages in polynomial time. The method is a general polynomial time reduction of learning a class of derived $ω$-tree languages to learning the underlying class of $ω$-word languages, for any class of $ω$-word languages recognized by a deterministic Büchi acceptor. Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli [1995] for the class of weak regular $ω$-word languages yields the main result. We also show that subset queries that return counterexamples can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or non-deterministic finite word acceptors, and deterministic or non-deterministic Büchi $ω$-word acceptors. A previous claim of an algorithm to learn regular $ω$-trees due to Jayasrirani, Begam and Thomas [2008] is unfortunately incorrect, as shown in Angluin [2016]. △ Less

Submitted 26 August, 2019; v1 submitted 13 February, 2018; originally announced February 2018.

Journal ref: Logical Methods in Computer Science, Volume 15, Issue 3 (August 27, 2019) lmcs:4311

SyGuS-Comp 2017: Results and Analysis

Authors: Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

Abstract: Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula phi in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-L… ▽ More Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula phi in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition six new solvers competed on over 1500 benchmarks. This paper presents and analyses the results of SyGuS-Comp'17. △ Less

Submitted 28 November, 2017; originally announced November 2017.

Comments: In Proceedings SYNT 2017, arXiv:1711.10224. arXiv admin note: text overlap with arXiv:1611.07627, arXiv:1602.01170

Journal ref: EPTCS 260, 2017, pp. 97-115

Proceedings Sixth Workshop on Synthesis

Authors: Dana Fisman, Swen Jacobs

Abstract: The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. App… ▽ More The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyber-physical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in particular application domains is encouraged. The sixth iteration of the workshop took place in Heidelberg, Germany. It was co-located with the 29th International Conference on Computer Aided Verification. The workshop included four contributed talks, four invited talks, and reports on the Syntax-Guided Synthesis Competition (SyGuS) and the Reactive Synthesis Competition (SYNTCOMP). △ Less

Submitted 28 November, 2017; originally announced November 2017.

Journal ref: EPTCS 260, 2017

Families of DFAs as Acceptors of $ω$-Regular Languages

Authors: Dana Angluin, Udi Boker, Dana Fisman

Abstract: Families of DFAs (FDFAs) provide an alternative formalism for recognizing $ω$-regular languages. The motivation for introducing them was a desired correlation between the automaton states and right congruence relations, in a manner similar to the Myhill-Nerode theorem for regular languages. This correlation is beneficial for learning algorithms, and indeed it was recently shown that $ω$-regular la… ▽ More Families of DFAs (FDFAs) provide an alternative formalism for recognizing $ω$-regular languages. The motivation for introducing them was a desired correlation between the automaton states and right congruence relations, in a manner similar to the Myhill-Nerode theorem for regular languages. This correlation is beneficial for learning algorithms, and indeed it was recently shown that $ω$-regular languages can be learned from membership and equivalence queries, using FDFAs as the acceptors. In this paper, we look into the question of how suitable FDFAs are for defining omega-regular languages. Specifically, we look into the complexity of performing Boolean operations, such as complementation and intersection, on FDFAs, the complexity of solving decision problems, such as emptiness and language containment, and the succinctness of FDFAs compared to standard deterministic and nondeterministic $ω$-automata. We show that FDFAs enjoy the benefits of deterministic automata with respect to Boolean operations and decision problems. Namely, they can all be performed in nondeterministic logarithmic space. We provide polynomial translations of deterministic Büchi and co-Büchi automata to FDFAs and of FDFAs to nondeterministic Büchi automata (NBAs). We show that translation of an NBA to an FDFA may involve an exponential blowup. Last, we show that FDFAs are more succinct than deterministic parity automata (DPAs) in the sense that translating a DPA to an FDFA can always be done with only a polynomial increase, yet the other direction involves an inevitable exponential blowup in the worst case. △ Less

Submitted 13 February, 2018; v1 submitted 24 December, 2016; originally announced December 2016.

ACM Class: F.1.1; D.2.4

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 1 (February 14, 2018) lmcs:2624

SyGuS-Comp 2016: Results and Analysis

Authors: Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

Abstract: Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $\varphi$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of… ▽ More Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $\varphi$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition we added a new track devoted to programming by examples. This track consisted of two categories, one using the theory of bit-vectors and one using the theory of strings. This paper presents and analyses the results of SyGuS-Comp'16. △ Less

Submitted 22 November, 2016; originally announced November 2016.

Comments: In Proceedings SYNT 2016, arXiv:1611.07178. arXiv admin note: text overlap with arXiv:1602.01170

ACM Class: I.2.2; D.1.2; D.2.2; D.2.4;

Journal ref: EPTCS 229, 2016, pp. 178-202

Results and Analysis of SyGuS-Comp'15

Authors: Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

Abstract: Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $\varphi$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of… ▽ More Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $\varphi$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations. Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB. The Syntax-Guided Synthesis Competition (SyGuS-comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks. In this year's competition we added two specialized tracks: a track for conditional linear arithmetic, where the grammar need not be specified and is implicitly assumed to be that of the LIA logic of SMT-LIB, and a track for invariant synthesis problems, with special constructs conforming to the structure of an invariant synthesis problem. This paper presents and analyzes the results of SyGuS-comp'15. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: In Proceedings SYNT 2015, arXiv:1602.00786

ACM Class: I.2.2, D.2.4, F.3.1;

Journal ref: EPTCS 202, 2016, pp. 3-26

Rational Synthesis

Authors: Dana Fisman, Orna Kupferman, Yoad Lustig

Abstract: Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system. Thus, it makes sense to model system environments not as hostile, but as composed of rational agents;… ▽ More Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system. Thus, it makes sense to model system environments not as hostile, but as composed of rational agents; i.e., agents that act to achieve their own objectives. We introduce the problem of synthesis in the context of rational agents (rational synthesis, for short). The input consists of a temporal-logic formula specifying the system and temporal-logic formulas specifying the objectives of the agents. The output is an implementation T of the system and a profile of strategies, suggesting a behavior for each of the agents. The output should satisfy two conditions. First, the composition of T with the strategy profile should satisfy the specification. Second, the strategy profile should be an equilibria in the sense that, in view of their objectives, agents have no incentive to deviate from the strategies assigned to them. We solve the rational-synthesis problem for various definitions of equilibria studied in game theory. We also consider the multi-valued case in which the objectives of the system and the agents are still temporal logic formulas, but involve payoffs from a finite lattice. △ Less

Submitted 17 July, 2009; originally announced July 2009.

Comments: 14 pages