research-article

TuLiP: a software toolbox for receding horizon temporal logic planning

Authors:

Tichakorn Wongpiromsarn,

Ufuk Topcu,

Necmiye Ozay,

Huan Xu,

Richard M. MurrayAuthors Info & Claims

HSCC '11: Proceedings of the 14th international conference on Hybrid systems: computation and control

Pages 313 - 314

https://doi.org/10.1145/1967701.1967747

Published: 12 April 2011 Publication History

Get Access

Abstract

This paper describes TuLiP, a Python-based software toolbox for the synthesis of embedded control software that is provably correct with respect to an expressive subset of linear temporal logic (LTL) specifications. TuLiP combines routines for (1) finite state abstraction of control systems, (2) digital design synthesis from LTL specifications, and (3) receding horizon planning. The underlying digital design synthesis routine treats the environment as adversary; hence, the resulting controller is guaranteed to be correct for any admissible environment profile. TuLiP applies the receding horizon framework, allowing the synthesis problem to be broken into a set of smaller problems, and consequently alleviating the computational complexity of the synthesis procedure, while preserving the correctness guarantee.

References

[1]

C. Finucane, G. Jing, and H. Kress-Gazit. LTLMoP. http://code.google.com/p/ltlmop/.

Google Scholar

[2]

B. Gerkey, R. Vaughan, and A. Howard. The Player/Stage project: Tools for multi-robot and distributed sensor systems. In Conf. on Advanced Robotics, 2003.

Google Scholar

[3]

S. Karaman and E. Frazzoli. Sampling-based motion planning with deterministic μ-calculus specifications. In IEEE CDC, 2009.

Crossref

Google Scholar

[4]

M. Kloetzer and C. Belta. LTLCon. http://iasi.bu.edu/~software/LTL-control.htm.

Google Scholar

[5]

M. Mazo, A. Davitian, and P. Tabuada. Pessoa: A tool for embedded controller synthesis. In T. Touili, B. Cook, and P. Jackson, editors, CAV, volume 6174 of LNCS, pages 566--569. Springer, 2010.

Digital Library

Google Scholar

[6]

N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In Verification, Model Checking and Abstract Interpretation, volume 3855 of LNCS, pages 364--380. Springer, 2006. http://jtlv.sourceforge.net/.

Digital Library

Google Scholar

[7]

P. Tabuada. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009.

Digital Library

Google Scholar

[8]

T. Wongpiromsarn, U. Topcu, and R. M. Murray. Automatic synthesis of robust embedded control software. In AAAI SS on Embedded Reasoning: Intelligence in Emb'd Systems, pages 104--111, 2010.

Google Scholar

[9]

T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon control for temporal logic specifications. In HSCC, pages 101--110, 2010.

Digital Library

Google Scholar

[10]

T. Wongpiromsarn, U. Topcu, and R. M. Murray. Formal synthesis of embedded control software: Application to vehicle management systems. In AIAA Infotech@Aerospace, 2011. submitted.

Google Scholar

[11]

B. Yordanov and C. Belta. conPAS2. http://hyness.bu.edu/conPAS2.html.

Google Scholar

Cited By

View all

Toscano-Moreno MMandow AMartínez MGarcía-Cerezo A(2024)SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation ModelsSensors10.3390/s2416516624:16(5166)Online publication date: 10-Aug-2024
https://doi.org/10.3390/s24165166
Sun YPoskitt CZhang XSun JRoychoudhury APaiva AAbreu RStorey M(2024)REDriver: Runtime Enforcement for Autonomous VehiclesProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639151(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639151
Gorenstein AMaoz SRingert JRoychoudhury APaiva AAbreu RStorey M(2024)Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) SpecificationsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3608131(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3608131
Show More Cited By

Index Terms

TuLiP: a software toolbox for receding horizon temporal logic planning
1. Software and its engineering
  1. Software creation and management
    1. Designing software
    2. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Receding horizon control for temporal logic specifications
HSCC '10: Proceedings of the 13th ACM international conference on Hybrid systems: computation and control

In this paper, we describe a receding horizon framework that satisfies a class of linear temporal logic specifications sufficient to describe a wide range of properties including safety, stability, progress, obligation, response and guarantee. The ...
Receding horizon H_∞ control problems for sampled-data systems

In this article, the receding horizon H_∞ control problems for sampled-data system are considered. Since sampled-data systems can be rewritten as equivalent jump systems, the receding horizon H_∞ control problems for time-varying jump systems are ...
Brief Robust one-step receding horizon control of discrete-time Markovian jump uncertain systems

This paper proposes a receding horizon control scheme for a set of uncertain discrete-time linear systems with randomly jumping parameters described by a finite-state Markov process whose jumping transition probabilities are assumed to belong to some ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

HSCC '11: Proceedings of the 14th international conference on Hybrid systems: computation and control

April 2011

330 pages

ISBN:9781450306294

DOI:10.1145/1967701

General Chair:
Marco Caccamo
University of Illinois at Urbana-Champaign, USA
,
Program Chairs:
Emilio Frazzoli
Massachusetts Institute of Technology, USA
,
Radu Grosu
State University of New York at Stony Brook, USA

Permission to make digital or hard copies of all or part 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 components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

IEEE

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 April 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

HSCC '11

Sponsor:

SIGBED

HSCC '11: Hybrid Systems: Computation and Control

April 12 - 14, 2011

IL, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

136
Total Citations
View Citations
688
Total Downloads

Downloads (Last 12 months)58
Downloads (Last 6 weeks)5

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Toscano-Moreno MMandow AMartínez MGarcía-Cerezo A(2024)SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation ModelsSensors10.3390/s2416516624:16(5166)Online publication date: 10-Aug-2024
Sun YPoskitt CZhang XSun JRoychoudhury APaiva AAbreu RStorey M(2024)REDriver: Runtime Enforcement for Autonomous VehiclesProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639151(1-12)Online publication date: 20-May-2024
Gorenstein AMaoz SRingert JRoychoudhury APaiva AAbreu RStorey M(2024)Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) SpecificationsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3608131(1-12)Online publication date: 20-May-2024
Ren WPan ZXia WSun X(2024)Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic QuantizationIEEE/CAA Journal of Automatica Sinica10.1109/JAS.2024.12447311:10(2082-2098)Online publication date: Oct-2024
Dai ZAsgharivaskasi ADuong TLin STzes MPappas GAtanasov N(2024)Optimal Scene Graph Planning with Large Language Model Guidance2024 IEEE International Conference on Robotics and Automation (ICRA)10.1109/ICRA57147.2024.10610599(14062-14069)Online publication date: 13-May-2024
Ehlers RKhalimov A(2024)Fully Generalized Reactivity(1) SynthesisTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_6(83-102)Online publication date: 4-Apr-2024
Fan C(2024)Formal Methods for Safe AutonomyundefinedOnline publication date: 11-Oct-2024
Miller KBrewer JSoderlund APhillips S(2023)Sensor Safety and Multi-Objective Satellite Control under Nonlinear Dynamics2023 American Control Conference (ACC)10.23919/ACC55779.2023.10156074(4284-4289)Online publication date: 31-May-2023
Calvagna AGhosh ASoudjnai S(2023)Using Knowledge Awareness to Improve Safety of Autonomous Driving2023 IEEE International Conference on Systems, Man, and Cybernetics (SMC)10.1109/SMC53992.2023.10394593(2997-3002)Online publication date: 1-Oct-2023
Badithela AWongpiromsarn TMurray R(2023)Evaluation Metrics of Object Detection for Quantitative System-Level Analysis of Safety-Critical Autonomous Systems2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)10.1109/IROS55552.2023.10342465(8651-8658)Online publication date: 1-Oct-2023
Show More Cited By

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

Receding horizon control for temporal logic specifications

Receding horizon H_∞ control problems for sampled-data systems

Brief Robust one-step receding horizon control of discrete-time Markovian jump uncertain systems