Article
Automation & Control Systems
Tiange Yang, Yuanyuan Zou, Shaoyuan Li, Yaru Yang
Summary: This paper proposes a distributed model predictive control (DMPC) approach for addressing discrete-time stochastic multi-agent systems with partially coupled temporal logic tasks. The approach utilizes probabilistic signal temporal logic (PrSTL) constraints and a shrinking horizon DMPC framework to control the coupled spatio-temporal relationship between agents and stochastic uncertainties. Additionally, the paper introduces a probabilistic-tightening method and a distributed PrSTL task softening method to reduce conservatism in controller design and optimize task completion.
IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING
(2023)
Article
Computer Science, Information Systems
Tatjana Kapus
Summary: This article presents an approach to formally verify the implementation of firewall rules in a network of SDN switches using TLA(+). The approach improves the efficiency of model checking and solves a specific problem regarding distributed firewalls.
Article
Robotics
Pian Yu, Yulong Gao, Frank J. Jiang, Karl H. Johansson, Dimos V. Dimarogonas
Summary: This paper studies the online control synthesis problem for uncertain discrete-time systems subject to signal temporal logic (STL) specifications. The authors propose an approach based on STL, reachability analysis, and temporal logic trees. They demonstrate the effectiveness of the approach through simulation examples and a hardware experiment.
INTERNATIONAL JOURNAL OF ROBOTICS RESEARCH
(2023)
Article
Automation & Control Systems
Lars Lindemann, Dimos V. Dimarogonas
Summary: Temporal logics have recently been shown to be valuable in various control applications as they provide a rich specification language. This paper introduces computationally-efficient funnel-based feedback control laws for systems with partially unknown dynamics to achieve robustness.
NONLINEAR ANALYSIS-HYBRID SYSTEMS
(2021)
Article
Computer Science, Hardware & Architecture
Siang-Yun Lee, Heinz Riener, Alan Mishchenko, Robert K. Brayton, Giovanni De Micheli
Summary: This article proposes a new logic synthesis and verification paradigm based on circuit simulation. By pregenerating high quality, expressive simulation patterns to be reused in multiple runs of optimization and verification algorithms, the paradigm reduces time-consuming Boolean computations such as SAT solving. The generated patterns are shown to be reusable across different algorithms and after network function modifications.
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
(2022)
Article
Automation & Control Systems
Shangtong Zhang, Shimon Whiteson
Summary: This paper addresses two open problems in emphatic TD methods by using truncated followon traces, reducing variance and enabling finite sample analysis for both prediction and control.
JOURNAL OF MACHINE LEARNING RESEARCH
(2022)
Article
Engineering, Aerospace
O. A. Jasim, S. M. Veres
Summary: A control system verification framework for unmanned aerial vehicles is proposed, aiming at proving the safety performance of the aircraft's mathematically designed control system under different environmental conditions. Mathematical derivations are checked for correctness using interactive and automated theorem-provers. The framework demonstrates the verification procedure by formally proving a nonlinear attitude control system of a generic multi-rotor UAV, and some of the methods derived can be implemented onboard for detecting controller breaches and taking necessary actions to ensure flight safety.
AERONAUTICAL JOURNAL
(2023)
Article
Computer Science, Artificial Intelligence
Jinglin Xu, Guangyi Chen, Nuoxing Zhou, Wei-Shi Zheng, Jiwen Lu
Summary: This paper presents a probabilistic framework for localizing unintentional action in videos by modeling the uncertainty of annotations. The proposed approach achieves significant improvement on the largest unintentional action dataset.
IEEE TRANSACTIONS ON IMAGE PROCESSING
(2022)
Article
Computer Science, Artificial Intelligence
Truong-Thang Nguyen, Viet-Hung Dang
Summary: This study introduces a highly efficient framework, iDANS, for Incremental Dynamic Analysis (IDA) of civil structures subjected to earthquakes. By utilizing a physical-induced data-driven surrogate model, the computational complexity can be significantly reduced, leading to improved efficiency.
APPLIED INTELLIGENCE
(2023)
Article
Computer Science, Theory & Methods
Nan Zhang, Zhenhua Duan, Cong Tian
Summary: This paper introduces a new temporal logic called Unified Temporal Logic (UTL), which combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). The syntax, semantics, logic laws, and normal forms of UTL formulas are defined and proved, demonstrating how UTL can be used to describe properties effectively. UTL supports both finite and infinite models (intervals) and enables the specification and verification of practical properties that are challenging to formalize in LTL and PPTL.
THEORETICAL COMPUTER SCIENCE
(2021)
Article
Engineering, Civil
Xiaohong Chen, Juan Zhang, Zhi Jin, Min Zhang, Tong Li, Xiang Chen, Tingliang Zhou
Summary: This article proposes an approach to empower domain experts with formal methods for verifying safety requirements' consistency, aiming to enhance time efficiency and productivity. The approach involves transforming natural requirements into formal models and using formal methods for verification. The effectiveness and time-saving benefits of this approach are validated through two practical case studies.
IEEE TRANSACTIONS ON INTELLIGENT TRANSPORTATION SYSTEMS
(2023)
Article
Robotics
Wataru Hashimoto, Kazumune Hashimoto, Shigemasa Takai
Summary: This letter presents a method for learning an RNN controller that maximizes the robustness of STL specifications. By introducing the concept of STL2vec, the controller can be efficiently constructed and validated through examples of path planning problem.
IEEE ROBOTICS AND AUTOMATION LETTERS
(2022)
Article
Automation & Control Systems
Maria Charitidou, Dimos V. Dimarogonas
Summary: This article proposes a continuous-time receding horizon control scheme that encodes the satisfaction of STL tasks using time-varying control barrier functions designed online, thus avoiding integer expressions. The recursive feasibility of the scheme is guaranteed by satisfying a time-varying terminal constraint that ensures task satisfaction with predetermined robustness. The effectiveness of the method is demonstrated in a multirobot simulation scenario.
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
(2023)
Article
Automation & Control Systems
Yulong Gao, Alessandro Abate, Frank J. Jiang, Mirco Giacobbe, Lihua Xie, Karl Henrik Johansson
Summary: The study proposes algorithms for model checking and control synthesis for discrete-time uncertain systems under linear temporal logic specifications. By constructing temporal logic trees, the algorithms provide underapproximations and overapproximations of LTL formulas. A controlled TLT can be constructed for controlled transition systems, allowing for online control synthesis and generation of feasible control inputs at each time step. The algorithms demonstrate generality and online scalability in both finite and infinite systems.
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
(2022)
Article
Green & Sustainable Science & Technology
Lars odegaard Bentsen, Narada Dilp Warakagoda, Roy Stenbro, Paal Engelstad
Summary: This study investigates uncertainty modeling in wind power forecasting using different parametric and non-parametric methods. Johnson's SU distribution is found to outperform Gaussian distributions in predicting wind power. This research contributes to the literature by introducing Johnson's SU distribution as a candidate for probabilistic wind forecasting.
JOURNAL OF CLEANER PRODUCTION
(2024)
