-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
Relatedness of the Incidence Decay with Exponential Adjustment (IDEA) Model, "Farr's Law" and Compartmental Difference Equation SIR Models
Authors:
Mauricio Santillana,
Ashleigh Tuite,
Tahmina Nasserie,
Paul Fine,
David Champredon,
Leonid Chindelevitch,
Jonathan Dushoff,
David Fisman
Abstract:
Mathematical models are often regarded as recent innovations in the description and analysis of infectious disease outbreaks and epidemics, but simple models have been in use for projection of epidemic trajectories for more than a century. We recently described a single equation model (the incidence decay with exponential adjustment, or IDEA, model) that can be used for short term forecasting. In…
▽ More
Mathematical models are often regarded as recent innovations in the description and analysis of infectious disease outbreaks and epidemics, but simple models have been in use for projection of epidemic trajectories for more than a century. We recently described a single equation model (the incidence decay with exponential adjustment, or IDEA, model) that can be used for short term forecasting. In the mid-19th century, Dr. William Farr developed a single equation approach (Farr's law) for epidemic forecasting. We show here that the two models are in fact identical, and can be expressed in terms of one another, and also in terms of a susceptible-infectious-removed (SIR) compartmental model with improving control. This demonstrates that the concept of the reproduction number, R0, is implicit to Farr's (pre-microbial era) work, and also suggests that control of epidemics, whether via behavior change or intervention, is as integral to the natural history of epidemics as is the dynamics of disease transmission.
△ Less
Submitted 3 March, 2016;
originally announced March 2016.
-
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.
-
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.