Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Abstract elided by the publisher.
1,553 papers · page 32 of 78
ML for ML: Learning Cost Semantics by Experiment
Abstract elided by the publisher.
Learning Symbolic Automata
Abstract elided by the publisher.
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size o…
Encodings of Bounded Synthesis
The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. As a result, bounded synthesis is de…
Bounded Quantifier Instantiation for Checking Inductive Invariants
Abstract elided by the publisher.
Lazy Automata Techniques for WS1S
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 whether its language is empty. The main novelty is to test the emptiness on the fly, while construct…
Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution)
Abstract elided by the publisher.
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution)
Abstract elided by the publisher.
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (Vpa). Vpa recognize a robust and algorithmically tractable fragment of context-free languages that is natural for modeling programs.
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution)
Abstract elided by the publisher.
Forester: From Heap Shapes to Automata Predicates - (Competition Contribution)
Abstract elided by the publisher.
Synthesis of Recursive ADT Transformations from Reusable Templates
Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which…
Optimal Translation of LTL to Limit Deterministic Automata
Abstract elided by the publisher.
Index Appearance Record for Transforming Rabin Automata into Parity Automata
Transforming deterministic \(\omega \)-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance …
Hierarchical Network Formation Games
Abstract elided by the publisher.
Validation, Synthesis and Optimization for Cyber-Physical Systems
Abstract elided by the publisher.
FlyFast: A Mean Field Model Checker
Abstract elided by the publisher.
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution)
Abstract elided by the publisher.
Fair Termination for Parameterized Probabilistic Concurrent Systems
We consider the problem of automatically verifying that a parameterized family of probabilistic concurrent systems terminates with probability one for all instances against adversarial schedulers. A parameterized family defines an infinite-state system: for each number n, the fam…