26,098 papers · page 488 of 1,305
Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack…
Abstract elided by the publisher.
We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders…
Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight al…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
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…
Abstract elided by the publisher.
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…
Abstract elided by the publisher.
Abstract elided by the publisher.
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.
Abstract elided by the publisher.
Abstract elided by the publisher.
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…
Abstract elided by the publisher.
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 …
Abstract elided by the publisher.