Nonuniform abstractions, refinement and controller synthesis with novel\n BDD encodings

2018/04/11 by Oscar Lindvall Bulancea, Bulancea, Oscar Lindvall, Petter Nilsson +3
Computer Science · Biochemistry, Genetics and Molecular Biology · #Formal Methods in Verification #Logic, programming, and type systems #Receptor Mechanisms and Signaling

paper · pdf · doi:10.48550/arxiv.1804.04280

Abstract

This paper presents a control synthesis algorithm for dynamical systems to\nsatisfy specifications given in a fragment of linear temporal logic. It is\nbased on an abstraction-refinement scheme with nonuniform partitions of the\nstate space. A novel encoding of the resulting transition system is proposed\nthat uses binary decision diagrams for efficiency. We discuss several factors\naffecting scalability and present some benchmark results demonstrating the\neffectiveness of the new encodings. These ideas are also being implemented on a\npublicly available prototype tool, ARCS, that we briefly introduce in the\npaper.\n

Citations

• Synthesis of Reactive(1) designs
• Graph-Based Algorithms for Boolean Function Manipulation

Related

• Abstraction-Based Output-Feedback Control with State-Based Specifications
• On Abstraction-Based Controller Design With Output Feedback
• Lazy Abstraction-Based Controller Synthesis
• Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs
• Abstractions for Symbolic Controller Synthesis are Composable