Dana Fisman

Most of the papers available here appear in print, and the corresponding copyright is held by the publisher. While the papers can be used for personal use, redistribution or reprinting for commercial purposes is prohibited.

Books

• A Practical Introduction to PSL

  Cindy Eisner and Dana Fisman

  Springer 2006.

Book Chapters

• Functional Specification of Hardware via Temporal Logic

  Cindy Eisner and Dana Fisman

  Chapter in Handbook of Model Checking 2018:795-829.
  
  abstract | pdf
  less | pdf

  Abstract:

  In the late seventies, Pnueli suggested that functional properties of reactive systems be formally expressed in temporal logic. In order that model checking such a logic be possible, it must have sufficient expressive power, its semantics must be formally defined in a rigorous way, and the complexity of model checking it must be well understood and reasonable. In order to allow widespread adoption in the industry, there is an additional requirement: functional specification must be made easy, allowing common properties to be expressed intuitively and succinctly. But while adding syntax is simple, defining semantics without breaking properties of the existing semantics is a different story. This chapter is about the various extensions to temporal logic included in the IEEE standards PSL and SVA, their motivation, and the subtle semantic issues encountered in their definition.

• Syntax-Guided Synthesis

  R. Alur, R. Bodik, E. Dallal, D. Fisman, P. Garg, G. Juniwal, H. Kress-Gazit, P. Madusudan, M. Martin, M. Raghothman, S. Saha , S. Seshia, R. Singh, A. Solar-Lezama, E. Torlak and A. Udupa in DSEE'15

  abstract | pdf | slides
  less | pdf

  Abstract:

  The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe alternative solution strategies that combine learning, counterexample analysis and constraint solving. We report on prototype implementations, and present experimental results on the set of benchmarks collected as part of the first SyGuS-Comp competition held in July 2014.

Refereed Publications

• A Normalized Edit Distance on Infinite Words

  Dana Fisman, Joshua Grogin and Gera Weiss in CSL'23

  abstract | pdf
  less | pdf

  Abstract:

  We introduce omega-ned, an edit distance between infinite words, that is a natural extension of ned, the normalized edit distance between finite words. We show it is a metric on (equivalence classes of) infinite words. We provide a polynomial time algorithm to compute the distance between two ultimately periodic words, and a polynomial time algorithm to compute the distance between two regular omega-languages given by non-deterministic Büchi automata.

• Learning and Characterizing Fully-Ordered Lattice Automata

  Dana Fisman and Sagi Saadon in ATVA'22

  abstract | pdf
  less | pdf

  Abstract:

  Traditional automata classify words from a given alphabet as either good or bad. In many scenarios, in particular in formal verification, a finer classification is required. Fully-ordered lattice automata (FOLA) associate with every possible word a value from a finite set of values such as {0,1,2,...,k}. In this paper we are interested in learning formal series that can be represented by FOLA. Such a series can be learned by a straight forward extension of the L* algorithm. However, this approach does not take advantage of the special structure of a FOLA. In this paper we investigate FOLAs and provide a Myhill-Nerode characterization for FOLAs, which serves as a basis for providing a specialized algorithm for FOLAs, which we term FOL*. We compare the performance of FOL* to that of L* on synthetically generated FOLA. Our experiments show that FOL* outperforms L* in the number of states of the obtained FOLA, the number of issued value queries (the extension of membership queries to the quantitative setting), and the number of issued equivalence queries.

• The Normalized Edit Distance with Uniform Operation Costs Is a Metric

  Dana Fisman, Joshua Grogin, Oded Margalit and Gera Weiss in CPM'22

  abstract | pdf
  less | pdf

  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 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.

• Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata

  Dana Angluin, Timos Antonopoulos, Dana Fisman and Nevin George in FoSSaCS'22

  abstract | pdf
  less | pdf

  Abstract:

  We explore the suitability of mod 2 multiplicity automata (M2MAs) as a representation for regular languages of infinite words. M2MAs are a deterministic representation that is known to be learnable in polynomial time with membership and equivalence queries, in contrast to many other representations. Another advantage of M2MAs compared to non-deterministic automata is that their equivalence can be decided in polynomial time and complementation incurs only an additive constant size increase. Because learning time is parameterized by the size of the representation, particular attention is focused on the relative succinctness of alternate representations, in particular, LTL formulas and Buchi automata of the types: deterministic, non-deterministic and strongly unambiguous. We supplement the theoretical results of worst case upper and lower bounds with experimental results computed for randomly generated automata and specific families of LTL formulas.

• Inferring Symbolic Automata

  Dana Fisman, Hadar Frenkel and Sandra Zilles in CSL'22

  abstract | pdf
  less | pdf

  Abstract:

  We study the learnability of symbolic finite state automata, 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. We provide a necessary condition and a sufficient condition for efficient learnability of SFAs in this paradigm, from which we derive a positive and a negative result.

• Learning of Structurally Unambiguous Probabilistic Grammars

  Dana Fisman, Dolav Nitay, Michal Ziv-Ukelson in AAAI'21, journal LMCS 2023

  abstract | pdf | journal
  less | pdf | journal

  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. 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.

• Learning Interpretable Models in the Property Specification Language

  Rajarshi Roy, Dana Fisman, Daniel Neider in IJCAI'20

  abstract | pdf
  less | pdf

  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). 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. The learning algorithm we designed, 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.

• Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries

  Dana Angluin, Timos Antonopoulos and Dana Fisman at CSL'20

  abstract | pdf
  less | pdf

  Abstract:

  A Büchi automaton is strongly unambiguous if every infinite word has at most one final path. Many properties of strongly unambiguous Büchi automata (SUBAs) are known. They are fully expressive: every regular ω-language can be represented by a SUBA. Equivalence and containment of SUBAs can be decided in polynomial time. SUBAs may be exponentially smaller than deterministic Muller automata and may be exponentially bigger than deterministic Büchi automata. In this work we show that SUBAs can be learned in polynomial time using membership and certain non-proper equivalence queries, which implies that they are polynomially predictable with membership queries. In contrast, under plausible cryptographic assumptions, non-deterministic Büchi automata are not polynomially predictable with membership queries.

• Polynomial Identification of omega-Automata

  Dana Angluin, Dana Fisman, Yaara Shoval at TACAS'20

  abstract | pdf
  less | pdf

  Abstract:

  We study identification in the limit using polynomial time and data for models of ω-automata. On the negative side we show that non-deterministic ω-automata (of types Büchi, coBüchi, Parity or Muller) can not be polynomially learned in the limit. On the positive side we show that the ω-language classes \IB, \IC, \IP, and \IM that are defined by deterministic Büchi, coBüchi, parity, and Muller acceptors that are isomorphic to their right-congruence automata (that is, the right congruences of languages in these classes are fully informative) are identifiable in the limit using polynomial time and data. We further show that for these classes a characteristic sample can be constructed in polynomial time.

• Streamable regular transductions

  Rajeev Alur, Dana Fisman, Konstantinos Mamouras, Mukund Raghothaman, Caleb Stanford at TCS, 2020

  abstract | pdf
  less | pdf

  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). 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 in 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.

• Query learning of derived 𝜔-tree languages in polynomial time.

  Dana Angluin, Timos Antonopoulos, Dana Fisman in LMCS 2019

  abstract | pdf
  less | pdf

  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 omega-tree languages derived from weak regular omega-word languages in polynomial time. The method is a general polynomial time reduction of learning a class of derived omega-tree languages to learning the underlying class of omega-word languages, for any class of omega-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 omega-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 omega-word acceptors. A previous claim of an algorithm to learn regular omega-trees due to Jayasrirani, Begam and Thomas [2008] is unfortunately incorrect, as shown in Angluin [2016].

• Search-based program synthesis

  Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama in CACM 2018

  abstract | pdf
  less | pdf

  Abstract:

  Writing programs that are both correct and efficient is challenging. A potential solution lies in program synthesis aimed at automatic derivation of an executable implementation (the "how") from a high-level logical specification of the desired input-to-output behavior (the "what"). A mature synthesis technology can have a transformative impact on programmer productivity by liberating the programmer from low-level coding details. For instance, for the classical computational problem of sorting a list of numbers, the programmer has to simply specify that given an input array A of n numbers, compute an output array B consisting of exactly the same numbers as A such that B[i] ≤ B[i + 1] for 1 ≤ i < n, leaving it to the synthesizer to figure out the sequence of steps needed for the desired computation.

  Traditionally, program synthesis is formalized as a problem in deductive theorem proving: A program is derived from the constructive proof of the theorem that states that for all inputs, there exists an output, such that the desired correctness specification holds. Building automated and scalable tools to solve this problem has proved to be difficult. A recent alternative to formalizing synthesis allows the programmer to supplement the logical specification with a syntactic template that constrains the space of allowed implementations and the solution strategies focus on search algorithms for efficiently exploring this space. The resulting search-based program synthesis paradigm is emerging as an enabling technology for both designing more intuitive programming notations and aggressive program optimizations.

• Temporal Reasoning on Incomplete Paths

  Dana Fisman and Hillel Kugler in ISoLA'18

  abstract | pdf | slides | talk
  less | pdf | slides | talk

  Abstract:

  Semantics of temporal logic over truncated paths (i.e. fi- nite paths that correspond to prefixes of computations of the system at hand) have been found useful in incomplete verification methods (such as bounded model checking and dynamic verification), in modeling hard- ware resets, and clock shifts and in online and offline monitoring of cyber-physical systems. In this paper we explore providing semantics for temporal logics on other types of incomplete paths, namely incomplete ultimately periodic paths, segmentally broken paths and combinations thereof. We review usages of temporal logic reasoning in systems biol- ogy, and explore whether systems biology can benefit from the suggested extensions.

• Regular ω-Languages with an Informative Right Congruence

  Dana Angluin and Dana Fisman in GandALF'18, journal at Inf. Comput. 2021

  abstract | pdf
  less | pdf

  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 ω-languages. The right congruence of a regular ω-language is not informative enough; many regular ω-languages have a trivial right congruence, and in general it is not always possible to define an ω-automaton recognizing a given language that is isomorphic to the rightcon automaton. The class of weak regular ω-languages does have an informative right congruence. That is, any weak regular ω-language can always be recognized by a deterministic Bu ̈chi automaton that is isomorphic to the rightcon automaton. Weak regular ω-languages reside in the lower levels of the expressiveness hierarchy of regular ω-languages. Are there more expressive sub-classes of regular ω-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.

• Inferring Regular Languages and ω-Languages

  Dana Fisman in JLAMP'18

  abstract | pdf
  less | pdf

  Abstract:

  In 1987 Angluin proposed an algorithm, termed L∗ for inferring an unknown regular language using membership and equivalence queries. This algorithm has found many applications, amongst which in the area of system design and verification. These applications challenge the state-of-the art solutions in various directions, in particular, scaling or working with more succinct representations, and dealing with ω-languages, the main model for reasoning about reactive systems.

  Both extensions confront a similar difficulty. Inference algorithms typically rely on the correspondence between the automata states and the right congruence, henceforth, the residuality property. DFAs enjoy the residuality property (as stated by the Myhill-Nerode Theorem) but more succinct representations such as non-deterministic and alternating finite automata (NFAs and AFAs) in general do not. The situation in the ω-languages realm is even worse, since none of the traditional automata that can express all regular ω-languages enjoys the residuality property.

  This paper surveys residual models for regular languages and ω-languages and the learning algorithms that can infer these models.

• Query Learning of Derived ω-Tree Languages in Polynomial Time

  Dana Angluin, Timos Antonopoulos and Dana Fisman in CSL'17

  abstract | pdf | slides
  less | pdfi | slides

  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 ω-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 in DBW. Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli [15] for the class of weak ω-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 nondeterministic 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 [11] is unfortunately incorrect, as shown in [4].

• SyGuS-Comp 2017: Results and Analysis

  Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama in SYNT'17

  abstract | pdf
  less | pdf

  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 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.

• Families of DFAs as Acceptors of ω-Regular Languages

  Dana Angluin, Udi Boker and Dana Fisman in MFCS'16, journal version at LMCS 2018

  abstract | pdf | journal
  less | pdf | journal

  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 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 ω-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.

• Regular Programming for Quantitative Properties of Data Streams

  Rajeev Alur, Dana Fisman and Mukund Raghothaman in ESOP'16

  abstract | pdf
  less | pdf

  Abstract:

  We propose regular cost expressions (RCEs) as a high-level programming abstraction for specifying complex numerical queries over data streams in a modular way. Our language allows the arbitrary nesting of orthogonal sets of combinators: (a) generalized versions of choice, concatenation, and Kleene-iteration from regular expressions, (b) streaming (serial) composition, and (c) numerical operators such as min, max, sum, difference, and averaging. Instead of requiring the programmer to figure out the low-level details of what state needs to be maintained and how to update it while processing each data item, the regular constructs facilitate a global view of the entire data stream splitting it into different cases and multiple chunks. The key technical challenge in defining our language is the design of typing rules that can be enforced efficiently and which strike a balance between expressiveness and theoretical guarantees for welltyped programs. We describe how to compile each RCE into an efficient streaming algorithm. The time and space complexity is dependent on the complexity of the data structure for representing terms over the basic numerical operators. In particular, we show that when the set of numerical operations is sum, difference, minimum, maximum, and average, the compiled algorithm uses constant space and processes each symbol in the data stream in constant time outputting the cost of the stream processed so far. Finally, we prove that the expressiveness of RCEs coincides with the streaming composition of regular functions, that is, MSO-definable string-to-term transformations, leading to a potentially robust foundation for understanding their expressiveness and the complexity of analysis problems.

• SyGuS-Comp 2016: Results and Analysis

  Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama in SYNT'16

  abstract | pdf
  less | pdf

  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 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.

• A Complexity Measure on Büchi Automata

  Dana Fisman in LATA'16

  abstract | pdf |
  less | pdf

  Abstract:

  We define a complexity measure on non-deterministic Büchi automata, based on the notion of the width of the skeleton tree introduced by Kahler and Wilke. We show that the induced hierarchy tightly correlates to the Wagner Hierarchy, a corner stone in the theory of regular omega-languages that is derived from a complexity measure on deterministic Muller automata. The relation between the hierarchies entails, for instance, that a nondeterministic Büchi automaton of width k can be translated to a deterministic parity automaton of degree at most 2k +1.

• Colored Nested Words

  Rajeev Alur and Dana Fisman in LATA'16

  abstract | pdf
  less | pdf | slides

  Abstract:

  Nested words allow modeling of linear and hierarchical structure in data, and nested word automata are special kinds of pushdown automata whose push/pop actions are directed by the hierarchical structure in the input nested word. The resulting class of regular languages of nested words has many appealing theoretical properties, and has found many applications, including model checking of procedural programs. In the nested word model, the hierarchical matching of open/close tags must be properly nested, and this is not the case, for instance, in program executions in presence of exceptions. This limitation of nested words narrows its model checking applications to programs with no exceptions.

  We introduce the model of colored nested words which allows such hierarchical structures with mismatches. We say that a language of colored nested words is regular if the language obtained by inserting the missing closing tags is a well-colored regular language of nested words. We define an automata model that accepts regular languages of colored nested words. These automata can execute restricted forms of "-pop transitions. We provide an equivalent grammar characterization and show that the class of regular languages of colored nested words has the same appealing closure and decidability properties as nested words, thus removing the restriction of programs to be exception-free in order to be amenable for model checking, via the nested words paradigm.

• Results and Analysis of SyGuS-Comp’15

  Rajeev Alur, Dana Fisman, Rishabh Singh and Armando Solar-Lezama in SYNT'15

  abstract | pdf
  less | pdf

  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-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.

• A Modular Approach for Büchi Determinization

  Dana Fisman and Yoad Lustig in CONCUR'15

  abstract | pdf | slides | talk
  less | pdf

  Abstract:

  The problem of Büchi determinization is a fundamental problem with important applications in reactive synthesis, multi-agent systems and probabilistic verification. The first asymptotically optimal Büchi determinization (a.k.a the Safra construction), was published in 1988. While asymptotically optimal, the Safra construction is notorious for its technical complexity and opaqueness in terms of intuition. While some improvements were published since the Safra construction, notably K¨ahler and Wilke’s construction, understanding the constructions remains a non-trivial task.

  In this paper we present a modular approach to Büchi determinization, where the difficulties are addressed one at a time, rather than simultaneously, making the solutions natural and easy to understand. We build on the notion of the skeleton trees of K¨ahler and Wilke. We first show how to construct a deterministic automaton in the case the skeleton’s width is one. Then we show how to construct a deterministic automaton in the case the skeleton’s width is k (for any given k). The overall construction is obtained by running in parallel the automata for all widths.

• Learning Regular Languages via Alternating Automata

  Dana Angluin, Sarah Eisenstat and Dana Fisman in IJCAI'15

  abstract | pdf | slides
  less | pdf

  Abstract:

  Nearly all algorithms for learning an unknown regular language, in particular the popular L* algorithm, yield deterministic finite automata. It was recently shown that the ideas of L* can be extended to yield non-deterministic automata, and that the respective learning algorithm, NL, outperforms L* on randomly generated regular expressions. We conjectured that this is due to the existential nature of regular expressions, and NL* might not outperform L* on languages with a universal nature. In this paper we introduce UL* — a learning algorithm for universal automata (the dual of nondeterministic automata); and AL* — a learning algorithm for alternating automata (which generalize both universal and non-deterministic automata). Our empirical results illustrate the advantages and trade-offs among L*, NL*, UL* and AL*.

• Learning Regular Omega Languages

  Dana Angluin and Dana Fisman in ALT'14, journal version at TCS 2016

  abstract | pdf | slides | journal
  less | pdf | journal

  Abstract:

  We provide an algorithm for learning an unknown regular set of infinite words, using membership and equivalence queries. Three variations of the algorithm learn three different canonical representations of omega regular languages, using the notion of families of DFAs. One is of size similar to L_$, a DFA representation recently learned using L* [Farzan et al.]. The second is based on the syntactic FORC, introduced in [Maler & Staiger]. The third is introduced herein. We show that the second can be exponentially smaller than the first, and the third is at most as large as the first two, with up to a quadratic saving with respect to the second.

• Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations

  Cindy Eisner, Dana Fisman and John Havlicek in TOCL 2014

  abstract | pdf
  less | pdf

  Abstract:

  We present a characterization that shows what it means for a formula to be a weak or strong version of another formula. We show that the weak version of a formula is not the same as Alpern and Schneider's safety component, but can be achieved by taking the closure in the Cantor topology over an augmented alphabet in which every formula is satisfiable. The resulting characterization allows us to show that the set of semantically weak formulas is exactly the set of non-pathological safety formulas. Furthermore, we use the characterization to show that the original versions of the IEEE standard temporal logics PSL and SVA are broken, and we show that the source of the problem lies in the semantics of the SERE intersection and fusion operators. Finally, we use the topological characterization to show the internal consistency of the alternative semantics adopted by the latest version of the PSL standard.

• SVA and PSL Local Variables - A Practical Approach

  Roy Armoni, Dana Fisman and Naiyong Jin in CAV'13

  abstract | pdf
  less | pdf

  Abstract:

  SystemVerilog Assertions (SVA), as well as Property Specification Language (PSL) are linear temporal logics based on LTL [14], extended with regular expressions and local variables. In [6] Bustan and Havlicek show that the local variable extensions, as well as regular expressions with intersection, render the verification problem of SVA and PSL formulae EXPSPACE-complete. In this paper we show a practical approach for the verification problem of SVA and PSL with local variables. We show that in practice, for a significant and meaningful subsets of those languages, which we denote PSL_pract, local variables do not increase the complexity of their verification problem, keeping it in PSPACE.

• Rational Synthesis

  Dana Fisman, Orna Kupferman and Yoad Lustig in TACAS'10

  abstract | pdf | slides
  less | pdf

  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; 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, temporal-logic formulas specifying the objectives of the agents, and a solution concept definition. 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 equilibrium in the sense that, in view of their objectives, agents have no incentive to deviate from the strategies assigned to them, where “no incentive to deviate” is interpreted as dictated by the given solution concept.

  We provide a method for solving the rational-synthesis problem, and show that for the classical definitions of equilibria studied in game theory, rational synthesis is not harder than traditional synthesis. 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.

• Reasoning about Finite-State Switched Systems

  Dana Fisman and Orna Kupferman in HVC'09

  abstract | pdf
  less | pdf

  Abstract:

  A switched system is composed of components. The components do not interact with one another. Rather, they all interact with the same environment, which switches one of them on at each moment in time. In standard concurrency, a component restricts the environment of the other components, thus the concurrent system has fewer behaviors than its components. On the other hand, in a switched system, a component suggests an alternative to the other components, thus the switched system has richer behaviors than its components.

  We study finite-state switched systems, where each of the underlying components is a finite-state transducer. While the main challenge, namely compositionality, is similar in standard concurrent systems and in switched systems, the problems and solutions are different. In the verification front, we suggest and study an assume guarantee paradigm for switched systems, and study formalisms in which satisfaction of a specification in all components imply its satisfaction in the switched system. In the synthesis front, we show that while compositional synthesis and design are undecidable, the problem of synthesizing a switching rule with which a given switched system satisfies an LTL specification is decidable.

• Augmenting a Regular Expression-Based Temporal Logic with Local Variables

  Cindy Eisner and Dana Fisman in FMCAD'08

  abstract | pdf
  less | pdf

  Abstract:

  The semantics of temporal logic is usually defined with respect to a word representing a computation path over a set of atomic propositions. A temporal logic formula does not control the behavior of the atomic propositions, it merely observes their behavior. Local variables are a twist on this approach, in which the user can declare variables local to the formula and control their behavior from within the formula itself.

  Local variables were introduced in 2002, and a formal semantics was given to them in the context of SVA, the assertion language of SystemVerilog, in 2004. That semantics suffers from several drawbacks. In particular, it breaks distributivity of the operators corresponding to intersection and union. In this paper we present a formal semantics for local variables that solves that problem and others, and compare it to the previous solution.

• A Framework for Inherent Vacuity

  Dana Fisman, Orna Kupferman, Sarai Sheinvald-Faragy and Moshe Vardi in HVC'08

  abstract | pdf
  less | pdf

  Abstract:

  Vacuity checking is traditionally performed after model checking has terminated successfully. It ensures that all the elements of the specification have played a role in its satisfaction by the design. Vacuity checking gets as input both design and specification, and is based on an in-depth investigation of the relation between them. Vacuity checking has been proven to be very useful in detecting errors in the modeling of the design or the specification. The need to check the quality of specifications is even more acute in property-based design, where the specification is the only input, serving as a basis to the development of the system.

  Current work on property assurance suggests various sanity checks, mostly based on satisfiability, non-validity, and realizability, but lacks a general framework for reasoning about the quality of specifications. We describe a framework for inherent vacuity, which carries the theory of vacuity in model checking to the setting of property-based design. Essentially, a specification is inherently vacuous if it can be mutated into a simpler equivalent specification, which we show to coincide with the fact the specification is satisfied vacuously in all systems. We also study the complexity of detecting inherent vacuity, and conclude that while inherent vacuity leads to specifications that better capture designer intent, it is not more complex than simple property-assurance checks.

• Structural Contradictions

  Cindy Eisner and Dana Fisman in HVC'08

  abstract | pdf
  less | pdf

  Abstract:

  We study the relation between logical contradictions such as p \and \not p and structural contradictions such as p \intersect (p · q). Intuitively, we expect the two to be treated similarly, but they are not by PSL, nor by SVA. We provide a solution that treats both kinds of contradictions in a consistent manner. The solution reveals that not all structural contradictions are created equal: we must distinguish between them in order to preserve important characteristics of the logic. An appealing result of our solution is that it provides the semantics over the natural alphabet 2^P , as opposed to the current semantics of PSL/SVA that use an inflated alphabet including the cryptic letters \top and \bot. We show that the complexity of model checking PSL/SVA is not affected by our proposed semantics.

• On Verifying Fault Tolerance of Distributed Protocols

  Dana Fisman, Orna Kupferman and Yoad Lustig in TACAS'08

  abstract | pdf
  less | pdf

  Abstract:

  Distributed systems are composed of processes connected in some network. Distributed systems may suffer from faults: processes may stop, may be interrupted, and may be maliciously attacked. Fault-tolerant protocols are designed to be resistant to faults. Proving the resistance of protocols to faults is a very challenging problem, as it combines the parameterized setting that distributed systems are based-on, with the need to consider a hostile environment that produces the faults. Considering all the possible fault scenarios for a protocol is very difficult. Thus, reasoning about fault tolerance protocols utterly needs formal methods.

  In this paper we describe a framework for verifying the fault tolerance of (synchronous or asynchronous) distributed protocols. In addition to the description of the protocol and the desired behavior, the user provides the fault type (e.g., fail-stop, Byzantine, ...) and its distribution (e.g., a strict minority of the processes are faulty, ...). Our framework is based on augmenting the description of the configurations of the system by a mask describing which processes are faulty. We focus on regular model checking and show how it is possible to compile the input for the model-checking problem to one that takes the faults and their distribution into an account, and perform regular model checking on the compiled input. We demonstrate the effectiveness of our framework and argue for its generality.

• Vacuity in Practice: Temporal Antecedent Failure

  Shoham Ben-David, Fady Copty, Dana Fisman and Sitvanit Ruah in FMSD 2015

  abstract | pdf
  less | pdf

  Abstract:

  Different definitions of vacuity in temporal logic model checking have been suggested along the years. Examining them closely, however, reveals an interesting phenomenon. On the one hand, some of the definitions require high-complexity vacuity detection algorithms. On the other hand, studies in the literature report that not all vacuities detected in practical applications are considered a problem by the system verifier. This brings vacuity detection into an undesirable situation where the user of the model checking tool may find herself waiting a long time for results that are of no interest for her. In this paper we restrict our attention to practical usage of vacuity detection. We define Temporal Antecedent Failure, an extension of antecedent failure to temporal logic, which refines the notion of vacuity. According to our experience, this type of vacuity always indicates a problem in the model, environment or property. We show how vacuity information can be derived from the automaton built for the original property, and we introduce the notion of vacuity explanation. Our experiments demonstrate that this type of vacuity as well as its reasons can be computed with a negligible increase in the overall runtime.

• Temporal Antecedent Failure: Refining Vacuity

  Shoham Ben-David, Dana Fisman and Sitvanit Ruah in CONCUR'07

  abstract | pdf
  less | pdf

  Abstract:

  We re-examine vacuity in temporal logic model checking. We note two disturbing phenomena in recent results in this area. The first indicates that not all vacuities detected in practical applications are considered a problem by the system verifier. The second shows that vacuity detection for certain logics can be very complex and time consuming. This brings vacuity detection into an undesirable situation where the user of the model checking tool may find herself waiting a long time for results that are of no interest for her.

  In this paper we define Temporal Antecedent Failure, an extension of antecedent failure to temporal logic, which refines the notion of vacuity. According to our experience, this type of vacuity always indicates a problem in the model, environment or formula. On top, detection of this vacuity is extremely easy to achieve. We base our definition and algorithm on regular expressions, that have become the major temporal logic specification in practical applications.

• On the Characterization of Until as a Fixed Point Under Clocked Semantics

  Dana Fisman in HVC'07

  abstract | pdf
  less | pdf

  Abstract:

  Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described in standard temporal logics, describing a multiply-clocked design is cumbersome. Thus, it is desirable to have an easier way to formulate properties related to clocks in a temporal logic. In [Eisner et al.] a relatively simple solution built on top of the traditional LTL semantics was suggested and adopted by the IEEE standard temporal logic PSL. The suggested semantics was examined relative to a list of design goals, and it was shown that it answered all requirements except for preserving the least fixed point characterization of the until operator under multiple clocks. In this work we show that with a minor addition to the semantics of [Eisner et al.] this requirement is met as well.

• The Safety Simple Subset

  Shoham Ben-David, Dana Fisman and Sitvanit Ruah in HVC'05

  abstract | pdf
  less | pdf

  Abstract:

  Regular-LTL (RLTL), extends LTL with regular expressions, and it is the core of the IEEE standard temporal logic PSL. Safety formulas of RLTL, as well as of other temporal logics, are easier to verify than other formulas. This is because verification of safety formulas can be reduced to invariance checking using an auxiliary automaton recognizing violating prefixes. In this paper we define a special subset of safety RLTL formulas, called RLTLLV, for which the automaton built is linear in the size of the formula. We then give two procedures for constructing such an automaton, the first provides a translation into a regular expression of linear size, while the second constructs the automaton directly from the given formula. We have derived the definition of RLTLLV by combining several results in the literature, and we devote a major part of the paper to reviewing these results and exploring the involved relationships.

• A Topological Characterization of Weakness

  Cindy Eisner, Dana Fisman and John Havlicek in PODC'05

  abstract | pdf
  less | pdf

  Abstract:

  We are interested in the relation between weak and strong temporal operators. We would like to find a characterization that shows what it means for an operator to be the weak or strong version of another operator, or more generally for a formula to be a weak or strong version of another formula. We show that the weak version of a formula is not the same as Alpern and Schneider's safety component. By working over an extended alphabet, we show that their topological characterization of safety can be adapted to obtain a topological characterization of weakness. We study the resulting topology and the relations between weak and strong formulas. Finally, we apply the method to show the internal consistency of a logic containing both weak and strong versions of regular expressions.

• Embedding Finite Automata within Regular Expressions

  Shoham Ben-David, Dana Fisman and Sitvanit Ruah in ISOLA'04, journal version at TCS 2008

  abstract | pdf
  less | pdf

  Abstract:

  Regular expressions and their extensions have become a major component of industry-oriented specification languages such as IEEE PSL [IEEE Standard for Property Specification Language (PSL), IEEE Std 1850TM-2005]. The model checking procedure of regular expression based formulas, involves constructing an automaton which runs in parallel with the model.

  In this paper we re-examine the automata construction. We propose an algorithm that allows an intermediate representation mixing both regular expressions and automata. This representation can be thought of as plugging an automaton inside a regular expression, to replace an existing sub-expression. In order to be verified, the intermediate representation is then translated into another automaton, resulting in a set of automata running in parallel. A key feature of this algorithm is that the plug-in automaton is independent of the regular expression from which it originated, and thus can be used in several different properties. We demonstrate the usefulness of our method by providing a set of applications. We show how the use of our method allows modularity and flexibility of the automata construction, and can increase expressiveness when seres are mixed with ctl. We give two applications for which it significantly reduces the size of the automata built for formulas, thus reducing the overall run time of the model checking procedure.

• Reasoning with Temporal Logic on Truncated Paths

  Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac and David Van Campenhout in CAV'03

  abstract | pdf
  less | pdf

  Abstract:

  We consider the problem of reasoning with linear temporal logic on truncated paths. A truncated path is a path which is finite, but not necessarily maximal. Truncated paths arise naturally in several areas, among which are incomplete verification methods (such as simulation or bounded model checking) and hardware resets. We present a formalism for reasoning about truncated paths, and analyze its characteristics.

• The Definition of a Temporal Clock Operator

  Cindy Eisner, Dana Fisman, John Havlicek, Anthony McIsaac and David Van Campenhout in ICALP'03

  abstract | pdf
  less | pdf

  Abstract:

  Modern hardware designs are typically based on multiple clocks. While a singly-clocked hardware design is easily described standard temporal logics, describing a multiply-clocked design is cumbersome. Thus it is desirable to have an easier way to formulate properties related to clocks in a temporal logic. We present a relatively simple solution built on top of the traditional LTL-based semantics, study the properties of the resulting logic, and compare it with previous solutions.

• The Temporal Logic Sugar

  Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, and Yoav Rodeh in CAV'01

  abstract | pdf
  less | pdf

  Abstract:

  Since the introduction of temporal logic for the specification of computer programs, usability has been an issue, because a difficult-to-use formalism is a barrier to the wide adoption of formal methods. Our solution is Sugar, the temporal logic used by the RuleBase formal verification tool. Sugar adds the power of regular expressions to CTL, as well as an extensive set of operators which provide syntactic sugar. That is, while these operators do not add expressive power, they allow properties to be expressed more succinctly than in the basic language. Experience shows that Sugar allows hardware engineers to easily and intuitively specify their designs. The full language is used for model checking, and a significant portion can be model checked on-the-fly. While previous papers have described various features of the language, this paper presents the first complete description of Sugar.

• Beyond Regular Model Checking

  Dana Fisman and Amir Pnueli in FSTTCS'01

  abstract | pdf
  less | pdf

  Abstract:

  In recent years it has been established that regular model checking can be successfully applied to several parameterized verification problems. However there are may parameterized verification problems that cannot be described by regular languages, and thus cannot be verified using regular model checking. In this study we try to practice symbolic model checking using classes of languages more expressive than regular languages. We provide three methods for the uniform verification of non-regular parameterized systems.

Techincal Reports

• Automata Construction for PSL

  Doron Bustan, Dana Fisman and John Havlicek Weizmann MCS05-04 report

  abstract | pdf
  less | pdf

  Abstract:

  The language PSL is a temporal logic standardized by the Accellera standards organization and currently undergoing the process of becoming an IEEE standard. The core of PSL, denoted here LTL_WR, is an extension of the linear temporal logic LTL. The extension takes two orthogonal directions. In one direction the logic is interpreted over finite, possibly truncated, as well as infinite words. In another direction, new basic formulas and operators are added to the language. The new basic formulas are weak and strong regular expressions, and the new operators are suffix conjunction/implication that combine regular expressions with other formulas.

  In this document we provide automata construction for LTL_WR. We show that for every LTL_WR formula f there exists a Buchi automaton whose size is exponential in the size of f. In addition, we classify the complexity of model checking simple properties of the regular expression layer. The suggested constructions can be used in the process of model checking psl properties using the automata-theoretic approach.