Synthesis of Infinite-State Systems with Random Behavior

TL;DR

This paper introduces a novel method for synthesizing infinite-state reactive systems with random behavior, enhancing diversity in responses while ensuring compliance with specifications, with applications in fuzz testing and robot motion planning.

Contribution

It presents a new Skolem extraction algorithm enabling the synthesis of witnesses with randomized behavior, expanding the capabilities of system synthesis.

Findings

Synthesized solutions meet specifications and exhibit diverse responses.

Framework effectively applies to model-based fuzz testing.

Synthesized controllers are practical for robot motion planning.

Abstract

Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification,while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed frame-work unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.