SemML 2.0: Synthesizing Controllers for LTL
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool SemML, which won this year's…
STL-Based Synthesis of Feedback Controllers Using Reinforcement Learning
Deep Reinforcement Learning (DRL) has the potential to be used for synthesizing feedback controllers (agents) for various complex systems with unknown dynamics. These systems are expected to satisfy diverse safety and li…
continuous-controlContinuous ControlDeep Reinforcement Learningreinforcement-learning+2Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets
In this paper, we propose an approach for synthesizing provable reach-avoid controllers, which drive a deterministic system operating in an unknown environment to safely reach a desired target set. The approach falls wit…
Synthesizing Decentralized Controllers with Graph Neural Networks and Imitation Learning
Dynamical systems consisting of a set of autonomous agents face the challenge of having to accomplish a global task, relying only on local information. While centralized controllers are readily available, they face limit…
Imitation LearningProbabilistic Learning of Torque Controllers from Kinematic and Force Constraints
When learning skills from demonstrations, one is often required to think in advance about the appropriate task representation (usually in either operational or configuration space). We here propose a probabilistic approa…