poster

OmegaThreads: symbolic controller design for ω-regular objectives

Authors:

Mahmoud Khaled,

Majid ZamaniAuthors Info & Claims

HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control

Article No.: 33, Pages 1 - 2

https://doi.org/10.1145/3447928.3457211

Published: 19 May 2021 Publication History

Get Access

Abstract

Increasing levels of autonomy in safety-critical systems such as autonomous vehicles, airplanes, and medical robots, pose questions about their safety, thus compelling the scientific community to provide novel techniques for the design of foolproof safety-critical control software (SCCS). One promising approach for designing formally-correct SCCS is to use unambiguous formal descriptions for design requirements and, at the same time, automate the development and implementation processes. In this poster, we introduce OmegaThreads [3], a tool for automated synthesis of formally-correct controllers for control systems from ω-regular specifications.

References

[1]

R. Ehlers and V. Raman. 2016. Slugs: Extensible GR(1) Synthesis. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 333--339.

Google Scholar

[2]

M. Khaled and M. Zamani. 2019. pFaces: An acceleration ecosystem for symbolic control. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC '19). ACM, New York, NY, USA.

Digital Library

Google Scholar

[3]

M. Khaled and M. Zamani. 2021. OmegaThreads: Symbolic Controller Design for ω-regular Objectives. In Proceedings of the 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC '21). ACM.

Google Scholar

[4]

M. Mazo, A. Davitian, and P. Tabuada. 2010. PESSOA: A Tool for Embedded Controller Synthesis. In Computer Aided Verification, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 566--569.

Digital Library

Google Scholar

[5]

P. J. Meyer, S. Sickert, and M. Luttenberger. 2018. Strix: Explicit Reactive Synthesis Strikes Back!. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 578--586.

Google Scholar

[6]

M. Rungger and M. Zamani. 2016. SCOTS: A Tool for the Synthesis of Symbolic Controllers. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC '16). ACM, New York, NY, USA, 99--104.

Digital Library

Google Scholar

Cited By

View all

Zhong BZamani MCaccamo M(2024)Formal Synthesis of Controllers for Uncertain Linear Systems Against -Regular Properties: A Set-Based ApproachIEEE Transactions on Automatic Control10.1109/TAC.2023.326739769:1(214-229)Online publication date: Jan-2024
https://doi.org/10.1109/TAC.2023.3267397
Juvvi MSundarsingh DDas RJagtap P(2024)Safe Multi-Robot Exploration using Symbolic Control2024 IEEE International Conference on Robotics and Automation (ICRA)10.1109/ICRA57147.2024.10610520(11619-11625)Online publication date: 13-May-2024
https://doi.org/10.1109/ICRA57147.2024.10610520
Murali VKalat SZamani M(2023)A Data-Driven Approach to Approximate Opacity Verification2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10384216(5085-5090)Online publication date: 13-Dec-2023
https://doi.org/10.1109/CDC49753.2023.10384216

Index Terms

OmegaThreads: symbolic controller design for ω-regular objectives
1. Computer systems organization
  1. Embedded and cyber-physical systems
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

OmegaThreads: symbolic controller design for ω-regular objectives
HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control

We introduce OmegaThreads, a tool for automatic synthesis of correct-by-construction controllers for control systems from ω-regular specifications. It accepts general nonlinear control systems from which discrete abstractions (a.k.a. symbolic models) ...
Dissecting ltlsynt
Abstract
ltlsynt is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. ltlsynt generally follows a textbook approach: the LTL specification is translated into a parity game whose winning strategy can be seen ...
Compositional Synthesis with Parametric Reactive Controllers
HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

Reactive synthesis with the ambitious goal of automatically synthesizing correct-by-construction controllers from high-level specifications, has recently attracted significant attention in system design and control. In practice, complex systems are ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control

May 2021

300 pages

ISBN:9781450383394

DOI:10.1145/3447928

Program Chairs:
Sergiy Bogomolov
Newcastle University, UK
,
Raphaël Jungers
UCLouvain, Belgium

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 May 2021

Check for updates

Author Tags

Qualifiers

Poster

Funding Sources

Conference

HSCC '21

Sponsor:

SIGBED

HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control

May 19 - 21, 2021

Tennessee, Nashville

Acceptance Rates

HSCC '21 Paper Acceptance Rate 27 of 77 submissions, 35%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
42
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zhong BZamani MCaccamo M(2024)Formal Synthesis of Controllers for Uncertain Linear Systems Against -Regular Properties: A Set-Based ApproachIEEE Transactions on Automatic Control10.1109/TAC.2023.326739769:1(214-229)Online publication date: Jan-2024
https://doi.org/10.1109/TAC.2023.3267397
Juvvi MSundarsingh DDas RJagtap P(2024)Safe Multi-Robot Exploration using Symbolic Control2024 IEEE International Conference on Robotics and Automation (ICRA)10.1109/ICRA57147.2024.10610520(11619-11625)Online publication date: 13-May-2024
https://doi.org/10.1109/ICRA57147.2024.10610520
Murali VKalat SZamani M(2023)A Data-Driven Approach to Approximate Opacity Verification2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10384216(5085-5090)Online publication date: 13-Dec-2023
https://doi.org/10.1109/CDC49753.2023.10384216
Sundarsingh DBhagiya JSaharsh Chatrola JSaoud AJagtap P(2023)Scalable Distributed Controller Synthesis for Multi-Agent Systems Using Barrier Functions and Symbolic Control2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10383476(6436-6441)Online publication date: 13-Dec-2023
https://doi.org/10.1109/CDC49753.2023.10383476

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

OmegaThreads: symbolic controller design for ω-regular objectives

Dissecting ltlsynt

Compositional Synthesis with Parametric Reactive Controllers