ref_temporal.bib

@article{beltaFormalMethodsControl2019a,
  title = {Formal {{Methods}} for {{Control Synthesis}}: {{An Optimization Perspective}}},
  shorttitle = {Formal {{Methods}} for {{Control Synthesis}}},
  author = {Belta, Calin and Sadraddini, Sadra},
  year = {2019},
  month = may,
  journal = {Annual Review of Control, Robotics, and Autonomous Systems},
  volume = {2},
  number = {Volume 2, 2019},
  pages = {115--140},
  publisher = {Annual Reviews},
  issn = {2573-5144},
  doi = {10.1146/annurev-control-053018-023717},
  url = {https://www.annualreviews.org/content/journals/10.1146/annurev-control-053018-023717},
  urldate = {2024-10-18},
  abstract = {In control theory, complicated dynamics such as systems of (nonlinear) differential equations are controlled mostly to achieve stability. This fundamental property, which can be with respect to a desired operating point or a prescribed trajectory, is often linked with optimality, which requires minimizing a certain cost along the trajectories of a stable system. In formal verification (model checking), simple systems, such as finite-state transition graphs that model computer programs or digital circuits, are checked against rich specifications given as formulas of temporal logics. The formal synthesis problem, in which the goal is to synthesize or control a finite system from a temporal logic specification, has recently received increased interest. In this article, we review some recent results on the connection between optimal control and formal synthesis. Specifically, we focus on the following problem: Given a cost and a correctness temporal logic specification for a dynamical system, generate an optimal control strategy that satisfies the specification. We first provide a short overview of automata-based methods, in which the dynamics of the system are mapped to a finite abstraction that is then controlled using an automaton corresponding to the specification. We then provide a detailed overview of a class of methods that rely on mapping the specification and the dynamics to constraints of an optimization problem. We discuss advantages and limitations of these two types of approaches and suggest directions for future research.},
  langid = {english}
}

@inproceedings{cimattiNUSMVNewSymbolic1999,
  title = {{{NUSMV}}: {{A New Symbolic Model Verifier}}},
  shorttitle = {{{NUSMV}}},
  booktitle = {Proceedings of the 11th {{International Conference}} on {{Computer Aided Verification}}},
  author = {Cimatti, Alessandro and Clarke, Edmund M. and Giunchiglia, Fausto and Roveri, Marco},
  year = {1999},
  month = jul,
  series = {{{CAV}} '99},
  pages = {495--499},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  url = {https://link.springer.com/content/pdf/10.1007/3-540-48683-6_44.pdf},
  urldate = {2022-08-27},
  isbn = {978-3-540-66202-0}
}

@inproceedings{donzeBluSTLControllerSynthesis2015,
  title = {{{BluSTL}}: {{Controller Synthesis}} from {{Signal Temporal Logic Specifications}}},
  shorttitle = {{{BluSTL}}},
  booktitle = {{{ARCH14-15}}. 1st and 2nd {{International Workshop}} on {{Applied veRification}} for {{Continuous}} and {{Hybrid Systems}}},
  author = {Donz{\'e}, Alexandre and Raman, Vasumathi},
  year = {2015},
  month = dec,
  pages = {160--150},
  doi = {10.29007/g39q},
  url = {https://doi.org/10.29007/g39q},
  urldate = {2025-01-07},
  abstract = {We present BluSTL, a MATLAB toolbox for generating controllers from             specifications written in Signal Temporal Logic (STL). The toolbox takes as input a system and a             set of constraints expressed in STL and constructs an open-loop or a closed-loop (in a receding             horizon or Model Predictive fashion) controller that enforces these constraints on the system             while minimizing some cost function. The controller can also be made reactive or robust to some             external input or disturbances.}
}

@inproceedings{donzeRobustSatisfactionTemporal2010,
  title = {Robust {{Satisfaction}} of {{Temporal Logic}} over {{Real-Valued Signals}}},
  booktitle = {Formal {{Modeling}} and {{Analysis}} of {{Timed Systems}}},
  author = {Donz{\'e}, Alexandre and Maler, Oded},
  editor = {Chatterjee, Krishnendu and Henzinger, Thomas A.},
  year = {2010},
  pages = {92--106},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-642-15297-9_9},
  abstract = {We consider temporal logic formulae specifying constraints in continuous time and space on the behaviors of continuous and hybrid dynamical system admitting uncertain parameters. We present several variants of robustness measures that indicate how far a given trajectory stands, in space and time, from satisfying or violating a property. We present a method to compute these robustness measures as well as their sensitivity to the parameters of the system or parameters appearing in the formula. Combined with an appropriate strategy for exploring the parameter space, this technique can be used to guide simulation-based verification of complex nonlinear and hybrid systems against temporal properties. Our methodology can be used for other non-traditional applications of temporal logic such as characterizing subsets of the parameter space for which a system is guaranteed to satisfy a formula with a desired robustness degree.},
  isbn = {978-3-642-15297-9},
  langid = {english}
}

@misc{donzeSignalTemporalLogic2013,
  type = {Lecture},
  title = {On {{Signal Temporal Logic}}},
  author = {Donz{\'e}, Alexandre},
  year = {2014},
  month = feb,
  address = {University of California, Berkeley},
  url = {https://people.eecs.berkeley.edu/~sseshia/fmee/lectures/EECS294-98_Spring2014_STL_Lecture.pdf},
  langid = {english}
}

@article{fainekosTemporalLogicMotion2009,
  title = {Temporal Logic Motion Planning for Dynamic Robots},
  author = {Fainekos, Georgios E. and Girard, Antoine and {Kress-Gazit}, Hadas and Pappas, George J.},
  year = {2009},
  month = feb,
  journal = {Automatica},
  volume = {45},
  number = {2},
  pages = {343--352},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2008.08.008},
  url = {https://www.sciencedirect.com/science/article/pii/S000510980800455X},
  urldate = {2024-10-18},
  abstract = {In this paper, we address the temporal logic motion planning problem for mobile robots that are modeled by second order dynamics. Temporal logic specifications can capture the usual control specifications such as reachability and invariance as well as more complex specifications like sequencing and obstacle avoidance. Our approach consists of three basic steps. First, we design a control law that enables the dynamic model to track a simpler kinematic model with a globally bounded error. Second, we built a robust temporal logic specification that takes into account the tracking errors of the first step. Finally, we solve the new robust temporal logic path planning problem for the kinematic model using automata theory and simple local vector fields. The resulting continuous time trajectory is provably guaranteed to satisfy the initial user specification.}
}

@article{farahaniRobustModelPredictive2015,
  title = {Robust {{Model Predictive Control}} for {{Signal Temporal Logic Synthesis}}},
  author = {Farahani, Samira S. and Raman, Vasumathi and Murray, Richard M.},
  year = {2015},
  month = jan,
  journal = {IFAC-PapersOnLine},
  series = {Analysis and {{Design}} of {{Hybrid Systems ADHS}}},
  volume = {48},
  number = {27},
  pages = {323--328},
  issn = {2405-8963},
  doi = {10.1016/j.ifacol.2015.11.195},
  url = {https://www.sciencedirect.com/science/article/pii/S2405896315024532},
  urldate = {2024-10-18},
  abstract = {Most automated systems operate in uncertain or adversarial conditions, and have to be capable of reliably reacting to changes in the environment. The focus of this paper is on automatically synthesizing reactive controllers for cyber-physical systems subject to signal temporal logic (STL) specifications. We build on recent work that encodes STL specifications as mixed integer linear constraints on the variables of a discrete-time model of the system and environment dynamics. To obtain a reactive controller, we present solutions to the worst-case model predictive control (MPC) problem using a suite of mixed integer linear programming techniques. We demonstrate the comparative effectiveness of several existing worst-case MPC techniques, when applied to the problem of control subject to temporal logic specifications; our empirical results emphasize the need to develop specialized solutions for this domain.}
}

@article{farahaniShrinkingHorizonModel2019,
  title = {Shrinking {{Horizon Model Predictive Control With Signal Temporal Logic Constraints Under Stochastic Disturbances}}},
  author = {Farahani, Samira S. and Majumdar, Rupak and Prabhu, Vinayak S. and Soudjani, Sadegh},
  year = {2019},
  month = aug,
  journal = {IEEE Transactions on Automatic Control},
  volume = {64},
  number = {8},
  pages = {3324--3331},
  issn = {1558-2523},
  doi = {10.1109/TAC.2018.2880651},
  url = {https://ieeexplore.ieee.org/abstract/document/8528869},
  urldate = {2025-01-07},
  abstract = {We present shrinking horizon model predictive control for discrete-time linear systems under stochastic disturbances with constraints encoded as signal temporal logic (STL) specification. The control objective is to satisfy a given STL specification with high probability against stochastic uncertainties while maximizing the robust satisfaction of an STL specification with minimum control effort. We formulate a general solution, which does not require precise knowledge of probability distributions of (possibly dependent) stochastic disturbances; only the bounded support of the density functions and moment intervals are used. For the specific case of disturbances that are normally distributed, we optimize the controllers by utilizing knowledge of the probability distribution of the disturbance. We show that in both cases, the control law can be obtained by solving optimization problems with linear constraints at each step. We experimentally demonstrate effectiveness of this approach by synthesizing a controller for a heating, ventilation, and air conditioning system.}
}

@inproceedings{finucaneLTLMoPExperimentingLanguage2010,
  title = {{{LTLMoP}}: {{Experimenting}} with Language, {{Temporal Logic}} and Robot Control},
  shorttitle = {{{LTLMoP}}},
  booktitle = {2010 {{IEEE}}/{{RSJ International Conference}} on {{Intelligent Robots}} and {{Systems}}},
  author = {Finucane, Cameron and Jing, Gangyuan and {Kress-Gazit}, Hadas},
  year = {2010},
  month = oct,
  pages = {1988--1993},
  issn = {2153-0866},
  doi = {10.1109/IROS.2010.5650371},
  abstract = {The Linear Temporal Logic MissiOn Planning (LTLMoP) toolkit is a software package designed to assist in the rapid development, implementation, and testing of high-level robot controllers. In this toolkit, structured English and Linear Temporal Logic are used to write high-level reactive task specifications, which are then automatically transformed into correct robot controllers that can be used to drive either a simulated or a real robot. LTLMoP's modular design makes it ideal for research in areas such as controller synthesis, semantic parsing, motion planning, and human-robot interaction.}
}

@book{fisherIntroductionPracticalFormal2011,
  title = {An {{Introduction}} to {{Practical Formal Methods Using Temporal Logic}}},
  author = {Fisher, Michael},
  year = {2011},
  month = apr,
  publisher = {Wiley},
  address = {Chichester, West Sussex, U.K. ; Hoboken, N.J},
  url = {https://www.wiley.com/en-us/An+Introduction+to+Practical+Formal+Methods+Using+Temporal+Logic-p-9780470027882},
  abstract = {The name "temporal logic" may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts - highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems. Fisher begins with a full introduction to the subject, covering the basics of temporal logic and using a variety of examples, exercises and pointers to more advanced work to help clarify and illustrate the topics discussed. He goes on to describe how this logic can be used to specify a variety of computational systems, looking at issues of linking specifications, concurrency, communication and composition ability. He then analyses temporal specification techniques such as deductive verification, algorithmic verification, and direct execution to develop and verify computational systems. The final chapter on case studies analyses the potential problems that can occur in a range of engineering applications in the areas of robotics, railway signalling, hardware design, ubiquitous computing, intelligent agents, and information security, and explains how temporal logic can improve their accuracy and reliability.     Models temporal notions and uses them to analyze computational systems     Provides a broad approach to temporal logic across many formal methods - including specification, verification and implementation     Introduces and explains freely available tools based on temporal logics and shows how these can be applied     Presents exercises and pointers to further study in each chapter, as well as an accompanying website providing links to additional systems based upon temporal logic as well as additional material related to the book.},
  isbn = {978-0-470-02788-2},
  langid = {english}
}

@article{gotzheinTemporalLogicApplications1992,
  title = {Temporal Logic and Applications---a Tutorial},
  author = {Gotzhein, Reinhard},
  year = {1992},
  month = may,
  journal = {Computer Networks and ISDN Systems},
  volume = {24},
  number = {3},
  pages = {203--218},
  issn = {0169-7552},
  doi = {10.1016/0169-7552(92)90109-4},
  url = {https://www.sciencedirect.com/science/article/pii/0169755292901094},
  urldate = {2022-07-09},
  abstract = {Temporal logic is a branch of formal logic which is of particular interest for the specification and verification of concurrent systems including communication services and protocols. This tutorial presents the principles of temporal logic and explains how it can be applied.},
  langid = {english}
}

@article{haesaertRobustDynamicProgramming2021,
  title = {Robust {{Dynamic Programming}} for {{Temporal Logic Control}} of {{Stochastic Systems}}},
  author = {Haesaert, Sofie and Soudjani, Sadegh},
  year = {2021},
  month = jun,
  journal = {IEEE Transactions on Automatic Control},
  volume = {66},
  number = {6},
  pages = {2496--2511},
  issn = {1558-2523},
  doi = {10.1109/TAC.2020.3010490},
  abstract = {Discrete-time stochastic systems are an essential modeling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we compute control strategies with lower- and upper-bounds for satisfying unbounded temporal logic specifications. First, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verification problem. These mappings yield a control strategy and a unique lower bound on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Second, upper-bounds on the satisfaction probability are quantified, and properties of the mappings are analyzed and discussed. Finally, we show the implications of these results to continuous state space of linear stochastic dynamic systems. This abstraction-based synthesis framework is shown to be able to handle infinite-horizon properties. Approximation errors expressed as deviations in the outputs of the models and as deviations in the probabilistic transitions are allowed and are quantified using approximate stochastic simulation relations.}
}

@misc{IEEEStandardProperty2010,
  type = {Standard},
  title = {{{IEEE Standard}} for {{Property Specification Language}} ({{PSL}})},
  year = {2010},
  month = apr,
  number = {1850},
  publisher = {IEEE},
  doi = {10.1109/IEEESTD.2010.5446004},
  url = {https://ieeexplore.ieee.org/document/5446004},
  urldate = {2025-01-02},
  abstract = {The IEEE Property Specification Language (PSL) is defined. PSL is a formal notation for specification of electronic system behavior, compatible with multiple electronic system design languages, including IEEE Std 1076{\textquestiondown} (VHDL{\textregistered}), IEEE Std 1354 (Verilog{\textregistered}), IEEE Std 1666{\textquestiondown} (SystemC{\textregistered}), and IEEE Std 1800{\textquestiondown} (SystemVerilog{\textregistered}), thereby enabling a common specification and verification flow for multi-language and mixed-language designs. PSL captures design intent in a form suitable for simulation, formal verification, formal analysis, and hybrid verification tools. PSL enhances communication among architects, designers, and verification engineers to increase productivity throughout the design and verification process. The primary audiences for this standard are the implementors of tools supporting the language and advanced users of the language.}
}

@misc{jiangGuaranteedCompletionComplex2024,
  title = {Guaranteed {{Completion}} of {{Complex Tasks}} via {{Temporal Logic Trees}} and {{Hamilton-Jacobi Reachability}}},
  author = {Jiang, Frank J. and Arfvidsson, Kaj Munhoz and He, Chong and Chen, Mo and Johansson, Karl H.},
  year = {2024},
  month = apr,
  number = {arXiv:2404.08334},
  eprint = {2404.08334},
  primaryclass = {cs, eess},
  publisher = {arXiv},
  doi = {10.48550/arXiv.2404.08334},
  url = {http://arxiv.org/abs/2404.08334},
  urldate = {2024-06-26},
  abstract = {In this paper, we present an approach for guaranteeing the completion of complex tasks with cyber-physical systems (CPS). Specifically, we leverage temporal logic trees constructed using Hamilton-Jacobi reachability analysis to (1) check for the existence of control policies that complete a specified task and (2) develop a computationally-efficient approach to synthesize the full set of control inputs the CPS can implement in real-time to ensure the task is completed. We show that, by checking the approximation directions of each state set in the temporal logic tree, we can check if the temporal logic tree suffers from the "leaking corner issue," where the intersection of reachable sets yields an incorrect approximation. By ensuring a temporal logic tree has no leaking corners, we know the temporal logic tree correctly verifies the existence of control policies that satisfy the specified task. After confirming the existence of control policies, we show that we can leverage the value functions obtained through Hamilton-Jacobi reachability analysis to efficiently compute the set of control inputs the CPS can implement throughout the deployment time horizon to guarantee the completion of the specified task. Finally, we use a newly released Python toolbox to evaluate the presented approach on a simulated driving task.},
  archiveprefix = {arXiv}
}

@inproceedings{kimDynamicContractsDistributed2017,
  title = {Dynamic Contracts for Distributed Temporal Logic Control of Traffic Networks},
  booktitle = {2017 {{IEEE}} 56th {{Annual Conference}} on {{Decision}} and {{Control}} ({{CDC}})},
  author = {Kim, Eric S. and Sadraddini, Sadra and Belta, Calin and Arcak, Murat and Seshia, Sanjit A.},
  year = {2017},
  month = dec,
  pages = {3640--3645},
  doi = {10.1109/CDC.2017.8264194},
  abstract = {Contract-based design is a method to synthesize distributed control strategies for large-scale networks of dynamically coupled systems. We propose a framework for using dynamic contracts for controlling traffic networks from temporal logic specifications. Given a traffic network, we partition it into a number of smaller sub-networks and compute a collection of assume-guarantee contracts for their dynamical interconnections. A central supervisor chooses the best contracts optimally according to the current state of the system. We use model predictive control (MPC) to find control sequences optimally for each sub-network subject to its contract obligations to and promises from its neighboring sub-networks. Our method is correct-by-design. A case study on a mixed urban-freeway network is presented, where the objective is infinite-time congestion avoidance and temporal requirements on the traffic lights in the urban intersections.}
}

@article{kloetzerFullyAutomatedFramework2008,
  title = {A {{Fully Automated Framework}} for {{Control}} of {{Linear Systems}} from {{Temporal Logic Specifications}}},
  author = {Kloetzer, Marius and Belta, Calin},
  year = {2008},
  month = feb,
  journal = {IEEE Transactions on Automatic Control},
  volume = {53},
  number = {1},
  pages = {287--297},
  issn = {1558-2523},
  doi = {10.1109/TAC.2007.914952},
  abstract = {We consider the following problem: given a linear system and a linear temporal logic (LTL) formula over a set of linear predicates in its state variables, find a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula. Our solution to this problem consists of three main steps. First, we partition the state space in accordance with the predicates in the formula, and construct a transition system over the partition quotient, which captures our capability of designing controllers. Second, using a procedure resembling model checking, we determine runs of the transition system satisfying the formula. Third, we generate the control strategy. Illustrative examples are included.}
}

@book{krogerTemporalLogicState2008,
  title = {Temporal {{Logic}} and {{State Systems}}},
  author = {Kr{\"o}ger, Fred and Merz, Stephan},
  year = {2008},
  series = {Texts in {{Theoretical Computer Science}}. {{An EATCS Series}}},
  publisher = {Springer},
  address = {Berlin; Heidelberg},
  url = {https://doi.org/10.1007/978-3-540-68635-4},
  isbn = {978-3-540-67401-6},
  langid = {english}
}

@inproceedings{kwonLTLCLinearTemporal2008,
  title = {{{LTLC}}: {{Linear Temporal Logic}} for {{Control}}},
  shorttitle = {{{LTLC}}},
  booktitle = {Hybrid {{Systems}}: {{Computation}} and {{Control}}},
  author = {Kwon, YoungMin and Agha, Gul},
  editor = {Egerstedt, Magnus and Mishra, Bud},
  year = {2008},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {316--329},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-540-78929-1_23},
  abstract = {Linear systems are one of the most commonly used models to represent physical systems. Yet, only few automated tools have been developed to check their behaviors over time. In this paper, we propose a linear temporal logic for specifying complex properties of discrete time linear systems. The proposed logic can also be used in a control system to generate control input in the process of model checking. Although, developing a full feedback control system is beyond the scope of this paper, authors believe that a feedback loop can be easily introduced by adopting the receding horizon scheme of predictive controllers. In this paper we explain the syntax, the semantics, a model checking algorithm, and an example application of our proposed logic.},
  isbn = {978-3-540-78929-1},
  langid = {english}
}

@article{lindemannControlBarrierFunctions2019,
  title = {Control {{Barrier Functions}} for {{Signal Temporal Logic Tasks}}},
  author = {Lindemann, Lars and Dimarogonas, Dimos V.},
  year = {2019},
  month = jan,
  journal = {IEEE Control Systems Letters},
  volume = {3},
  number = {1},
  pages = {96--101},
  issn = {2475-1456},
  doi = {10.1109/LCSYS.2018.2853182},
  url = {https://ieeexplore.ieee.org/abstract/document/8404080/?casa_token=vwXPjpyc0N0AAAAA:ooAsVpdTBi6zoxwz7VfKDD9ax0r4o08A5GpgxumGze35zMMaVlGOOAeCKoIm1Dn_QPiVAsBmGa0},
  urldate = {2024-12-18},
  abstract = {The need for computationally-efficient control methods of dynamical systems under temporal logic tasks has recently become more apparent. Existing methods are computationally demanding and hence often not applicable in practice. Especially with respect to multi-robot systems, these methods do not scale computationally. In this letter, we propose a framework that is based on control barrier functions and signal temporal logic. In particular, timevarying control barrier functions are considered where the temporal properties are used to satisfy signal temporal logic tasks. The resulting controller is given by a switching strategy between a computationally-efficient convex quadratic program and a local feedback control law.}
}

@article{lindemannReactiveRiskAwareControl2022,
  title = {Reactive and {{Risk-Aware Control}} for {{Signal Temporal Logic}}},
  author = {Lindemann, Lars and Pappas, George J. and Dimarogonas, Dimos V.},
  year = {2022},
  month = oct,
  journal = {IEEE Transactions on Automatic Control},
  volume = {67},
  number = {10},
  pages = {5262--5277},
  issn = {1558-2523},
  doi = {10.1109/TAC.2021.3120681},
  url = {https://ieeexplore.ieee.org/document/9576605},
  urldate = {2024-12-18},
  abstract = {The deployment of autonomous systems in uncertain and dynamic environments has raised fundamental questions. Addressing these is pivotal to build fully autonomous systems and requires a systematic integration of planning and control. We first propose reactive risk signal interval temporal logic (ReRiSITL) as an extension of signal temporal logic (STL) to formulate complex spatiotemporal specifications. Unlike STL, ReRiSITL allows to consider uncontrollable propositions that may model humans as well as random environmental events such as sensor failures. Additionally, ReRiSITL allows to incorporate risk measures, such as (but not limited to) the conditional value-at-risk, to measure the risk of violating certain spatial specifications. Second, we propose an algorithm to check if an ReRiSITL specification is satisfiable. For this purpose, we abstract the ReRiSITL specification into a timed signal transducer and devise a game-based approach. Third, we propose a reactive planning and control framework for dynamical control systems under ReRiSITL specifications.}
}

@article{lindemannRobustControlSignal2019,
  title = {Robust Control for Signal Temporal Logic Specifications Using Discrete Average Space Robustness},
  author = {Lindemann, Lars and Dimarogonas, Dimos V.},
  year = {2019},
  month = mar,
  journal = {Automatica},
  volume = {101},
  pages = {377--387},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2018.12.022},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109818306289},
  urldate = {2024-10-18},
  abstract = {Control systems that satisfy temporal logic specifications have become increasingly popular due to their applicability to robotic systems. Existing control methods, however, are computationally demanding, especially when the problem size becomes too large. In this paper, a robust and computationally efficient model predictive control framework for signal temporal logic specifications is proposed. We introduce discrete average space robustness, a novel quantitative semantic for signal temporal logic, that is directly incorporated into the cost function of the model predictive controller. The optimization problem entailed in this framework can be written as a convex quadratic program when no disjunctions are considered and results in a robust satisfaction of the specification. Furthermore, we define the predicate robustness degree as a new robustness notion. Simulations of a multi-agent system subject to complex specifications demonstrate the efficacy of the proposed method.}
}

@inproceedings{liuAbstractionDiscretizationRobustness2014,
  title = {Abstraction, Discretization, and Robustness in Temporal Logic Control of Dynamical Systems},
  booktitle = {Proceedings of the 17th International Conference on {{Hybrid}} Systems: Computation and Control},
  author = {Liu, Jun and Ozay, Necmiye},
  year = {2014},
  month = apr,
  series = {{{HSCC}} '14},
  pages = {293--302},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/2562059.2562137},
  url = {https://doi.org/10.1145/2562059.2562137},
  urldate = {2021-06-22},
  abstract = {Abstraction-based, hierarchical approaches to control synthesis from temporal logic specifications for dynamical systems have gained increased popularity over the last decade. Yet various issues commonly encountered and extensively dealt with in control systems have not been adequately discussed in the context of temporal logic control of dynamical systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and un-modeled dynamics, and the use of time-discretized models to design controllers for continuous-time dynamical systems. We discuss these issues in this paper. The main motivation is to demonstrate the possibility of accounting for the mismatches between a continuous-time control system and its various types of abstract models used for control synthesis. We do this by incorporating additional robustness measures in the abstract models. Such robustness measures are gained at the price of either increased non-determinism in the abstracted models or relaxed versions of the specification being realized. Under a unified notion of abstraction, we provide concrete means of incorporating these robustness measures and establish results that demonstrate their effectiveness in dealing with the above mentioned issues.},
  isbn = {978-1-4503-2732-9}
}

@article{liuFiniteAbstractionsRobustness2016,
  title = {Finite Abstractions with Robustness Margins for Temporal Logic-Based Control Synthesis},
  author = {Liu, Jun and Ozay, Necmiye},
  year = {2016},
  month = nov,
  journal = {Nonlinear Analysis: Hybrid Systems},
  volume = {22},
  pages = {1--15},
  issn = {1751-570X},
  doi = {10.1016/j.nahs.2016.02.002},
  url = {https://www.sciencedirect.com/science/article/pii/S1751570X16000169},
  urldate = {2021-06-22},
  abstract = {This paper introduces a notion of finite abstractions that can be used to synthesize robust controllers for dynamical systems from temporal logic specifications. These finite abstractions, equipped with certain robustness margins, provide a unified approach to various issues commonly encountered in implementing control systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and unmodeled dynamics. The main results of this paper demonstrate that the robustness margins can effectively account for the mismatches between a control system and its finite abstractions used for control synthesis. The quantitative nature of the robustness margins also makes it possible to study the trade-offs between the performance of controllers and their robustness against various types of adversaries (e.g., delays, measurement errors, or modeling uncertainties). We use a simple adaptive cruise control (ACC) example to illustrate such robustness--performance trade-offs.},
  langid = {english}
}

@inproceedings{liuSwitchingControlDynamical2014,
  title = {Switching Control of Dynamical Systems from Metric Temporal Logic Specifications},
  booktitle = {2014 {{IEEE International Conference}} on {{Robotics}} and {{Automation}} ({{ICRA}})},
  author = {Liu, Jun and Prabhakar, Pavithra},
  year = {2014},
  month = may,
  pages = {5333--5338},
  issn = {1050-4729},
  doi = {10.1109/ICRA.2014.6907643},
  abstract = {Motivated by designing high-level planners for dynamical systems (such as mobile robots) to achieve complex tasks, we consider the synthesis of switching controllers of nonlinear dynamical systems from metric temporal logic (MTL) specifications. MTL is a popular logic that allows to specify timed properties of real-time reactive systems and hence is appropriate for describing the safe and autonomous operations of robotic systems in an uncertain and possibly adversarial environment. We provide constructive means for computing finite-state abstractions that preserve MTL properties for nonlinear systems, under a weak assumption that these nonlinear systems evolve continuously with respect to their initial conditions. We then provide conditions to ensure that the existence of a discrete strategy (obtained by solving a discrete synthesis problem) guarantees the existence of a switching strategy for controlling the continuous-time dynamical systems to satisfy a given MTL specification. We illustrate the results on a motion planning problem.}
}

@inproceedings{malerMonitoringTemporalProperties2004,
  title = {Monitoring {{Temporal Properties}} of {{Continuous Signals}}},
  booktitle = {Formal {{Techniques}}, {{Modelling}} and {{Analysis}} of {{Timed}} and {{Fault-Tolerant Systems}}},
  author = {Maler, Oded and Nickovic, Dejan},
  editor = {Lakhnech, Yassine and Yovine, Sergio},
  year = {2004},
  pages = {152--166},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-540-30206-3_12},
  abstract = {In this paper we introduce a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic mitl, augmented with a static mapping from continuous domains into propositions. From formulae in this logic we create automatically property monitors that can check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation of this procedure was used to check properties of simulation traces generated by Matlab/Simulink.},
  isbn = {978-3-540-30206-3},
  langid = {english}
}

@book{mannaTemporalLogicReactive2012,
  title = {The {{Temporal Logic}} of {{Reactive}} and {{Concurrent Systems}}: {{Specification}}},
  shorttitle = {The {{Temporal Logic}} of {{Reactive}} and {{Concurrent Systems}}},
  author = {Manna, Zohar and Pnueli, Amir},
  year = {2012},
  month = dec,
  publisher = {Springer Science \& Business Media},
  abstract = {Reactive systems are computing systems which are interactive, such as real-time systems, operating systems, concurrent systems, control systems, etc. They are among the most difficult computing systems to program. Temporal logic is a formal tool/language which yields excellent results in specifying reactive systems. This volume, the first of two, subtitled Specification, has a self-contained introduction to temporal logic and, more important, an introduction to the computational model for reactive programs, developed by Zohar Manna and Amir Pnueli of Stanford University and the Weizmann Institute of Science, Israel, respectively.},
  googlebooks = {R0PtBwAAQBAJ},
  isbn = {978-1-4612-0931-7},
  langid = {english}
}

@misc{murrayLectureLinearTemporal2020,
  type = {Lecture},
  title = {Lecture 3 {{Linear Temporal Logic}} ({{LTL}})},
  author = {Murray, Richard M and Topcu, Ufuk and Wongpiromsarn, Nok},
  year = {2020},
  month = mar,
  address = {Belgrade (Serbia)},
  url = {http://www.cds.caltech.edu/~murray/courses/eeci-sp2020/L3_ltl-09Mar2020.pdf},
  langid = {english}
}

@inproceedings{ostroffStateMachinesTemporal1987,
  title = {State Machines, Temporal Logic and Control: {{A}} Framework for Discrete Event Systems},
  shorttitle = {State Machines, Temporal Logic and Control},
  booktitle = {26th {{IEEE Conference}} on {{Decision}} and {{Control}}},
  author = {Ostroff, J. S. and Wonham, W. M.},
  year = {1987},
  month = dec,
  volume = {26},
  pages = {681--686},
  doi = {10.1109/CDC.1987.272455},
  abstract = {A framework is proposed for investigating the verification and synthesis of controllers for real-time discrete event systems. In the framework, plants and controllers are modelled with extended state machines (ESMs), and a real-time temporal logic (RTL) is used for specification of required plant behaviour and for verifying that controllers satisfy their specifications. Controllers are implemented as tasks in a real-time distributed programming language. This paper discusses the issues of modelling and specification.}
}

@inproceedings{ostroffTemporalLogicApproach1985,
  title = {A Temporal Logic Approach to Real Time Control},
  booktitle = {1985 24th {{IEEE Conference}} on {{Decision}} and {{Control}}},
  author = {Ostroff, J. S. and Wonham, W. M.},
  year = {1985},
  month = dec,
  pages = {656--657},
  doi = {10.1109/CDC.1985.268574},
  abstract = {Discrete event systems in such areas as process control, flexible manufacturing systems and computer networks require real time distributed computer control to ensure an orderly flow of events. A temporal logic framework for the specification, analysis and verification of such control systems is discussed. Controllers are implemented in the Pascal based distributed language CONIC.}
}

@inproceedings{ramanModelPredictiveControl2014,
  title = {Model Predictive Control from Signal Temporal Logic Specifications: A Case Study},
  shorttitle = {Model Predictive Control from Signal Temporal Logic Specifications},
  booktitle = {Proceedings of the 4th {{ACM SIGBED International Workshop}} on {{Design}}, {{Modeling}}, and {{Evaluation}} of {{Cyber-Physical Systems}}},
  author = {Raman, Vasumathi and Maasoumy, Mehdi and Donz{\'e}, Alexandre},
  year = {2014},
  month = apr,
  series = {{{CyPhy}} '14},
  pages = {52--55},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/2593458.2593472},
  url = {https://dl.acm.org/doi/10.1145/2593458.2593472},
  urldate = {2024-10-18},
  abstract = {This paper describes current work on framing the model predictive control (MPC) of cyber-physical systems as synthesis from signal temporal logic (STL) specifications. We provide a case study using a simplified power grid model with uncertain demand and generation; the model-predictive control problem here is that of the ancillary service power flow from the buildings. We show how various relevant constraints can be captured using STL formulas, and incorporated into an MPC framework. We also provide preliminary simulation results to illustrate the promise of the proposed approach.},
  isbn = {978-1-4503-2871-5}
}

@inproceedings{ramanReactiveSynthesisSignal2015,
  title = {Reactive Synthesis from Signal Temporal Logic Specifications},
  booktitle = {Proceedings of the 18th {{International Conference}} on {{Hybrid Systems}}: {{Computation}} and {{Control}}},
  author = {Raman, Vasumathi and Donz{\'e}, Alexandre and Sadigh, Dorsa and Murray, Richard M. and Seshia, Sanjit A.},
  year = {2015},
  month = apr,
  series = {{{HSCC}} '15},
  pages = {239--248},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/2728606.2728628},
  url = {https://dl.acm.org/doi/10.1145/2728606.2728628},
  urldate = {2024-12-17},
  abstract = {We present a counterexample-guided inductive synthesis approach to controller synthesis for cyber-physical systems subject to signal temporal logic (STL) specifications, operating in potentially adversarial nondeterministic environments. We encode STL specifications as mixed integer-linear constraints on the variables of a discrete-time model of the system and environment dynamics, and solve a series of optimization problems to yield a satisfying control sequence. We demonstrate how the scheme can be used in a receding horizon fashion to fulfill properties over unbounded horizons, and present experimental results for reactive controller synthesis for case studies in building climate control and autonomous driving.},
  isbn = {978-1-4503-3433-4}
}

@inproceedings{renZonotopebasedControllerSynthesis2021,
  title = {Zonotope-Based {{Controller Synthesis}} for {{LTL Specifications}}},
  booktitle = {2021 60th {{IEEE Conference}} on {{Decision}} and {{Control}} ({{CDC}})},
  author = {Ren, Wei and Calbert, Julien and Jungers, Rapha{\"e}l},
  year = {2021},
  month = dec,
  pages = {580--585},
  issn = {2576-2370},
  doi = {10.1109/CDC45484.2021.9683150},
  abstract = {This paper studies the controller synthesis problem for Linear Temporal Logic (LTL) specifications using (constrained) zonotope techniques. First, we implement (constrained) zonotope techniques to partition the state space and further to verify whether the LTL specification can be satisfied. Once the LTL specification can be satisfied, the next step is to design a controller to guarantee the satisfaction of the LTL specification for dynamic systems. Based on the verification of the LTL specification, an abstraction-based control design approach is proposed in this paper: a novel abstraction construction is developed first, then finite local abstract controllers are designed to achieve the LTL specification, and finally the designed abstract controllers are combined and refined as the controller for the original system. The proposed control strategy is illustrated via a numerical example from autonomous robots.}
}

@article{tabuadaLinearTimeLogic2006,
  title = {Linear {{Time Logic Control}} of {{Discrete-Time Linear Systems}}},
  author = {Tabuada, Paulo and Pappas, George J.},
  year = {2006},
  month = dec,
  journal = {IEEE Transactions on Automatic Control},
  volume = {51},
  number = {12},
  pages = {1862--1877},
  issn = {1558-2523},
  doi = {10.1109/TAC.2006.886494},
  abstract = {The control of complex systems poses new challenges that fall beyond the traditional methods of control theory. One of these challenges is given by the need to control, coordinate and synchronize the operation of several interacting submodules within a system. The desired objectives are no longer captured by usual control specifications such as stabilization or output regulation. Instead, we consider specifications given by linear temporal logic (LTL) formulas. We show that existence of controllers for discrete-time controllable linear systems and LTL specifications can be decided and that such controllers can be effectively computed. The closed-loop system is of hybrid nature, combining the original continuous dynamics with the automatically synthesized switching logic required to enforce the specification}
}

@article{ulusoyRecedingHorizonTemporal2014,
  title = {Receding Horizon Temporal Logic Control in Dynamic Environments},
  author = {Ulusoy, Alphan and Belta, Calin},
  year = {2014},
  month = oct,
  journal = {The International Journal of Robotics Research},
  volume = {33},
  number = {12},
  pages = {1593--1607},
  publisher = {SAGE Publications Ltd STM},
  issn = {0278-3649},
  doi = {10.1177/0278364914537008},
  url = {https://doi.org/10.1177/0278364914537008},
  urldate = {2021-06-22},
  abstract = {We present a receding horizon method for controlling an autonomous vehicle that must satisfy a rich mission specification over service requests occurring at the regions of a partitioned environment. The overall mission specification consists of a temporal logic statement over a set of static, a priori known requests, a regular expression over a set of dynamic requests that can be sensed only locally, and a servicing priority order over these dynamic requests. Our approach is based on two main steps. First, we construct an abstraction for the motion of the vehicle in the environment by using input--output linearization and assignment of vector fields to the regions in the partition. Second, a receding horizon controller computes local plans within the sensing range of the vehicle such that both local and global mission specifications are satisfied. We implement and evaluate our method through experiments and simulations consisting of a quadrotor performing a persistent surveillance task over a planar grid environment.},
  langid = {english}
}

@phdthesis{wolffControlDynamicalSystems2014,
  title = {Control of {{Dynamical Systems}} with {{Temporal Logic Specifications}}},
  author = {Wolff, Eric M},
  year = {2014},
  address = {Pasadena, California},
  url = {https://thesis.library.caltech.edu/8078/1/wolff_eric_thesis.pdf},
  abstract = {This thesis is motivated by safety-critical applications involving autonomous air, ground, and space vehicles carrying out complex tasks in uncertain and adversarial environments. We use temporal logic as a language to formally specify complex tasks and system properties. Temporal logic specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Given a system model and a formal task specification, the goal is to automatically synthesize a control policy for the system that ensures that the system satisfies the specification. This thesis presents novel control policy synthesis algorithms for optimal and robust control of dynamical systems with temporal logic specifications. Furthermore, it introduces algorithms that are efficient and extend to high-dimensional dynamical systems.},
  langid = {english},
  school = {California Institute of Technology}
}

@techreport{wolffOptimalControlMixed2013,
  type = {Technical Report},
  title = {Optimal {{Control}} of {{Mixed Logical Dynamical Systems}} with {{Long-Term Temporal Logic Specifications}}},
  author = {Wolff, Eric M. and Murray, Richard M.},
  year = {2013},
  month = jun,
  number = {CaltechCDSTR:2013.001},
  address = {Pasadena, California},
  institution = {California Institute of Technology},
  url = {https://resolver.caltech.edu/CaltechCDSTR:2013.001},
  urldate = {2022-12-07},
  abstract = {We present a mathematical programming-based method for control of large a class of nonlinear systems subject to temporal logic task specifications. We consider Mixed Logical Dynamical (MLD) systems, which include linear hybrid automata, constrained linear systems, and piecewise affine systems. We specify tasks using a fragment of linear temporal logic (LTL) that allows both finite- and infinite-horizon properties to be specified, including tasks such as surveillance, periodic walking, repeated assembly, and environmental monitoring. Our method directly encodes an LTL formula as mixed-integer linear constraints on the MLD system, instead of computing a finite abstraction. This approach is efficient; for common tasks the formulation may use significantly fewer binary variables than related approaches. In simulation, we solve non-trivial temporal logic motion planning tasks for high-dimensional continuous systems using our approach.},
  copyright = {other},
  langid = {english}
}

@inproceedings{wongpiromsarnRecedingHorizonControl2010,
  title = {Receding Horizon Control for Temporal Logic Specifications},
  booktitle = {Proceedings of the 13th {{ACM}} International Conference on {{Hybrid}} Systems: Computation and Control},
  author = {Wongpiromsarn, Tichakorn and Topcu, Ufuk and Murray, Richard M.},
  year = {2010},
  month = apr,
  series = {{{HSCC}} '10},
  pages = {101--110},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/1755952.1755968},
  url = {https://doi.org/10.1145/1755952.1755968},
  urldate = {2021-06-22},
  abstract = {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 resulting embedded control software consists of a goal generator, a trajectory planner, and a continuous controller. The goal generator essentially reduces the trajectory generation problem to a sequence of smaller problems of short horizon while preserving the desired system-level temporal properties. Subsequently, in each iteration, the trajectory planner solves the corresponding short-horizon problem with the currently observed state as the initial state and generates a feasible trajectory to be implemented by the continuous controller. Based on the simulation property, we show that the composition of the goal generator, trajectory planner and continuous controller and the corresponding receding horizon framework guarantee the correctness of the system. To handle failures that may occur due to a mismatch between the actual system and its model, we propose a response mechanism and illustrate, through an example, how the system is capable of responding to certain failures and continues to exhibit a correct behavior.},
  isbn = {978-1-60558-955-8}
}

@article{wongpiromsarnRecedingHorizonTemporal2012,
  title = {Receding {{Horizon Temporal Logic Planning}}},
  author = {Wongpiromsarn, Tichakorn and Topcu, Ufuk and Murray, Richard M.},
  year = {2012},
  month = nov,
  journal = {IEEE Transactions on Automatic Control},
  volume = {57},
  number = {11},
  pages = {2817--2830},
  issn = {1558-2523},
  doi = {10.1109/TAC.2012.2195811},
  abstract = {We present a methodology for automatic synthesis of embedded control software that incorporates a class of linear temporal logic (LTL) specifications sufficient to describe a wide range of properties including safety, stability, progress, obligation, response and guarantee. To alleviate the associated computational complexity of LTL synthesis, we propose a receding horizon framework that effectively reduces the synthesis problem into a set of smaller problems. The proposed control structure consists of a goal generator, a trajectory planner, and a continuous controller. The goal generator reduces the trajectory generation problem into a sequence of smaller problems of short horizon while preserving the desired system-level temporal properties. Subsequently, in each iteration, the trajectory planner solves the corresponding short-horizon problem with the currently observed state as the initial state and generates a feasible trajectory to be implemented by the continuous controller. Based on the simulation property, we show that the composition of the goal generator, trajectory planner and continuous controller and the corresponding receding horizon framework guarantee the correctness of the system with respect to its specification regardless of the environment in which the system operates. In addition, we present a response mechanism to handle failures that may occur due to a mismatch between the actual system and its model. The effectiveness of the proposed technique is demonstrated through an example of an autonomous vehicle navigating an urban environment. This example also illustrates that the system is not only robust with respect to exogenous disturbances but is also capable of properly handling violation of the environment assumption that is explicitly stated as part of the system specification.}
}

@inproceedings{wongpiromsarnTuLiPSoftwareToolbox2011,
  title = {{{TuLiP}}: A Software Toolbox for Receding Horizon Temporal Logic Planning},
  shorttitle = {{{TuLiP}}},
  booktitle = {Proceedings of the 14th International Conference on {{Hybrid}} Systems: Computation and Control},
  author = {Wongpiromsarn, Tichakorn and Topcu, Ufuk and Ozay, Necmiye and Xu, Huan and Murray, Richard M.},
  year = {2011},
  month = apr,
  series = {{{HSCC}} '11},
  pages = {313--314},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/1967701.1967747},
  url = {https://doi.org/10.1145/1967701.1967747},
  urldate = {2021-08-06},
  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.},
  isbn = {978-1-4503-0629-4}
}

@article{yangSignalTemporalLogic2024,
  title = {Signal Temporal Logic Synthesis under {{Model Predictive Control}}: {{A}} Low Complexity Approach},
  shorttitle = {Signal Temporal Logic Synthesis under {{Model Predictive Control}}},
  author = {Yang, Tiange and Zou, Yuanyuan and Li, Shaoyuan and Yin, Xiang and Jia, Tianyu},
  year = {2024},
  month = feb,
  journal = {Control Engineering Practice},
  volume = {143},
  pages = {105782},
  issn = {0967-0661},
  doi = {10.1016/j.conengprac.2023.105782},
  url = {https://www.sciencedirect.com/science/article/pii/S0967066123003519},
  urldate = {2025-01-02},
  abstract = {In this paper, we focus on the challenging problem of model predictive control (MPC) for dynamics systems with high-level tasks formulated as signal temporal logic (STL). The state-of-art for STL synthesis mainly suffers from limited scalability with respect to the complexity of the task and the planning horizon, hindering the real-time implementation of MPC. This work tackles this issue by STL formula reformulation and input blocking. Specifically, simplifications are applied on disjunctive STL (sub)formulae recursively in the framework of MPC to limit formula size. We show that the simplified STL can be reformulated into mixed integer linear programming (MILP) constraints with a modifiable number of binary variables being required. The move blocking scheme is then employed to further reduce problem complexity by fixing input variables to be constant over several time intervals. In order to trade off the control performance and computational load, a blocking structure design with on-line correction is proposed. The extension of the proposed STL-MPC algorithm to uncertain systems is achieved through STL constraint tightening. Simulations and experiments show the effectiveness of the proposed algorithm.}
}

@article{yordanovTemporalLogicControl2012,
  title = {Temporal {{Logic Control}} of {{Discrete-Time Piecewise Affine Systems}}},
  author = {Yordanov, Boyan and Tumova, Jana and Cerna, Ivana and Barnat, Ji{\v r}{\'i} and Belta, Calin},
  year = {2012},
  month = jun,
  journal = {IEEE Transactions on Automatic Control},
  volume = {57},
  number = {6},
  pages = {1491--1504},
  issn = {1558-2523},
  doi = {10.1109/TAC.2011.2178328},
  abstract = {We present a computational framework for automatic synthesis of a feedback control strategy for a discrete-time piecewise affine (PWA) system from a specification given as a linear temporal logic (LTL) formula over an arbitrary set of linear predicates in the system's state variables. Our approach consists of two main steps. First, by defining appropriate partitions for its state and input spaces, we construct a finite abstraction of the PWA system in the form of a control transition system. Second, by leveraging ideas and techniques from LTL model checking and Rabin games, we develop an algorithm to generate a control strategy for the finite abstraction. While provably correct and robust to state measurements and small perturbations in the applied inputs, the overall procedure is conservative and expensive. The proposed algorithms have been implemented as a software package and made available for download. Illustrative examples are included.}
}

@article{yuContinuousTimeControlSynthesis2024,
  title = {Continuous-{{Time Control Synthesis Under Nested Signal Temporal Logic Specifications}}},
  author = {Yu, Pian and Tan, Xiao and Dimarogonas, Dimos V.},
  year = {2024},
  journal = {IEEE Transactions on Robotics},
  volume = {40},
  pages = {2272--2286},
  issn = {1941-0468},
  doi = {10.1109/TRO.2024.3353081},
  url = {https://ieeexplore.ieee.org/document/10388467},
  urldate = {2025-01-03},
  abstract = {In this work, we propose a novel approach for the continuous-time control synthesis of nonlinear systems under nested signal temporal logic (STL) specifications. While the majority of existing literature focuses on control synthesis for STL specifications without nested temporal operators, addressing nested temporal operators poses a notably more challenging scenario and requires new theoretical advancements. Our approach hinges on the concepts of STL tree (sTLT) and control barrier function (CBF). Specifically, we detail the construction of an sTLT from a given STL formula and a continuous-time dynamical system, the sTLT semantics (i.e., satisfaction condition), and the equivalence or underapproximation relation between sTLT and STL. Leveraging the fact that the satisfaction condition of an sTLT is essentially keeping the state within certain sets during certain time intervals, it provides explicit guidelines for the CBF design. The resulting controller is obtained through the utilization of an online CBF-based program coupled with an event-triggered scheme for online updating the activation time interval of each CBF, with which the correctness of the system behavior can be established by construction. We demonstrate the efficacy of the proposed method for single-integrator and unicycle models under nested STL formulas.}
}

@article{yuOnlineControlSynthesis2024,
  title = {Online Control Synthesis for Uncertain Systems under Signal Temporal Logic Specifications},
  author = {Yu, Pian and Gao, Yulong and Jiang, Frank J. and Johansson, Karl H. and Dimarogonas, Dimos V.},
  year = {2024},
  month = may,
  journal = {The International Journal of Robotics Research},
  volume = {43},
  number = {6},
  pages = {765--790},
  publisher = {SAGE Publications Ltd STM},
  issn = {0278-3649},
  doi = {10.1177/02783649231212572},
  url = {https://doi.org/10.1177/02783649231212572},
  urldate = {2024-12-18},
  abstract = {Signal temporal logic (STL) formulas have been widely used as a formal language to express complex robotic specifications, thanks to their rich expressiveness and explicit time semantics. Existing approaches for STL control synthesis suffer from limited scalability with respect to the task complexity and lack of robustness against the uncertainty, for example, external disturbances. In this paper, we study the online control synthesis problem for uncertain discrete-time systems subject to STL specifications. Different from existing techniques, we propose an approach based on STL, reachability analysis, and temporal logic trees. First, based on a real-time version of STL semantics, we develop the notion of tube-based temporal logic tree (tTLT) and its recursive (offline) construction algorithm. We show that the tTLT is an under-approximation of the STL formula, in the sense that a trajectory satisfying a tTLT also satisfies the corresponding STL formula. Then, an online control synthesis algorithm is designed using the constructed tTLT. It is shown that when the STL formula is robustly satisfiable and the initial state of the system belongs to the initial root node of the tTLT, it is guaranteed that the trajectory generated by the control synthesis algorithm satisfies the STL formula. We validate the effectiveness of the proposed approach by several simulation examples and further demonstrate its practical usability on a hardware experiment. These results show that our approach is able to handle complex STL formulas with long horizons and ensure the robustness against the disturbances, which is beyond the scope of the state-of-the-art STL control synthesis approaches.},
  langid = {english}
}