3 citations · 16 across the 22 of their papers we have counts for
23 papers
Complementing Emerson-Lei Elevator Automata (Technical Report)
Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál +2
Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected compone…
A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report)
Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál +1
Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint…
Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)
Vojtěch Havlena, Ondřej Lengál, Yong Li +2
Complementation of nondeterministic Büchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis…
An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report)
Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál +3
We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a triple and the question is whether, giv…
Word Equations in Synergy with Regular Constraints (Technical Report)
František Blahoudek, Yu-Fang Chen, David Chocholatý +4
When eating spaghetti, one should have the sauce and noodles mixed instead of eating them separately. We argue that also in string solving, word equations and regular constraints a…
Complementing Büchi Automata with Ranker (Technical Report)
Vojtěch Havlena, Ondřej Lengál, Barbora Šmahlíková
We present the tool Ranker for complementing Büchi automata (BAs). Ranker builds on our previous optimizations of rank-based BA complementation and pushes them even further using n…
Towards Efficient Matching of Regexes with Backreferences using Register Set Automata (Technical Report)
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál +2
Matching regexes (regular expressions) is a common problem in many areas of computer science, with requirements on high speed and robust performance. Regexes with backreferences al…
Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation (Technical Report)
Vojtěch Havlena, Ondřej Lengál, Barbora Šmahlíková
We propose several heuristics for mitigating one of the main causes of combinatorial explosion in rank-based complementation of Büchi automata (BAs): unnecessarily high bounds on t…
Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)
Vojtěch Havlena, Ondřej Lengál
This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe's theoretically optimal construction and develop a set o…
Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report)
Lukáš Holík, Ondřej Lengál, Olli Saarikivi +3
We propose an efficient algorithm for determinising counting automata (CAs), i.e., finite automata extended with bounded counters. The algorithm avoids unfolding counters into cont…
Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál +1
We propose a lazy decision procedure for the logic WSkS. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical W…
Simulations in Rank-Based Büchi Automata Complementation (Technical Report)
Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál
Complementation of Büchi automata is an essential technique used in some approaches for termination analysis of programs. The long search for an optimal complementation constructio…
Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata
Milan Češka, Vojtěch Havlena, Lukáš Holík +6
Deep packet inspection via regular expression (RE) matching is a crucial task of network intrusion detection systems (IDSes), which secure Internet connection against attacks and s…
Simulation Algorithms for Symbolic Automata (Technical Report)
Lukáš Holík, Ondřej Lengál, Juraj Síč +2
We investigate means of efficient computation of the simulation relation over symbolic finite automata (SFAs), i.e., finite automata with transitions labeled by predicates over alp…
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report)
Ondrej Lengal, Anthony W. Lin, Rupak Majumdar +1
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversa…
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection (Technical Report)
Milan Ceska, Vojtech Havlena, Lukas Holik +2
We consider the problem of approximate reduction of non-deterministic automata that appear in hardware-accelerated network intrusion detection systems (NIDSes). We define an error…
Register automata with linear arithmetic
Yu-Fang Chen, Ondrej Lengal, Tony Tan +1
We propose a novel automata model over the alphabet of rational numbers, which we call register automata over the rationals (RA-Q). It reads a sequence of rational numbers and outp…
An Executable Sequential Specification for Spark Aggregation
Yu-Fang Chen, Chih-Duo Hong, Ondřej Lengál +3
Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregat…
Lazy Automata Techniques for WS1S
Tomáš Fiedor, Lukáš Holík, Petr Janků +2
We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests…
PAC Learning-Based Verification and Model Synthesis
Yu-Fang Chen, Chiao Hsieh, Ondřej Lengál +4
We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning a regular model of the set of feasible paths in a pro…
Nested Antichains for WS1S
Tomas Fiedor, Lukas Holik, Ondrej Lengal +1
We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within t…
Fully Automated Shape Analysis Based on Forest Automata
Lukas Holik, Ondrej Lengal, Adam Rogalewicz +2
Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples…
An Efficient Finite Tree Automata Library
Ondřej Lengál
Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with so…