1 citations · 1 across the 3 of their papers we have counts for
6 papers · 1 filter
Negated String Containment is Decidable (Technical Report)
Vojtěch Havlena, Michal Hečko, Lukáš Holík +1
We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbol…
A Uniform Framework for Handling Position Constraints in String Solving (Technical Report)
Yu-Fang Chen, Vojtěch Havlena, Michal Hečko +2
We introduce a novel decision procedure for solving the class of position string constraints, which includes string disequalities, not-prefixof, not-suffixof, strat, and not-str…
Complementation of Emerson-Lei Automata (Technical Report)
Vojtěch Havlena, Ondřej Lengál, Barbora Šmahlíková
We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a special…
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…
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…
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…