Article
Automation & Control Systems
Xiaoyi Zhou, Tiange Yang, Yuanyuan Zou, Shaoyuan Li, Hao Fang
Summary: This article investigates the temporal logic problem for multiagent systems, introducing a two-step distributed model predictive control (DMPC) strategy to maximize the number of satisfied subtasks and minimize the violation degree of unsatisfied ones. The proposed algorithm ensures the satisfaction verification of coupled subtasks and guarantees soundness and feasibility.
IEEE TRANSACTIONS ON INDUSTRIAL ELECTRONICS
(2023)
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
Daiying Tian, Hao Fang, Qingkai Yang, Zixuan Guo, Jinqiang Cui, Wenyu Liang, Yan Wu
Summary: This article studies the planning problem for a robot residing in partially unknown environments under signal temporal logic (STL) specifications. A novel two-phase planning method is proposed to efficiently synthesize paths that satisfy STL tasks, namely offline exploration followed by online planning. The proposed method reduces computational burden and avoids collisions with unknown obstacles.
IEEE TRANSACTIONS ON INDUSTRIAL ELECTRONICS
(2023)
Article
Computer Science, Information Systems
Meiyi Ma, Ezio Bartocci, Eli Lifland, John A. Stankovic, Lu Feng
Summary: This article introduces a novel spatial-temporal specification-based monitoring system for smart cities, which develops a new spatial aggregation STL for efficient runtime monitoring of city requirements. Through a study of over 1000 smart city requirements, the article proposes two new logical operators to enhance STL for expressing spatial aggregation and spatial counting characteristics.
IEEE INTERNET OF THINGS JOURNAL
(2021)
Article
Computer Science, Hardware & Architecture
Zhenya Zhang, Paolo Arcaini, Xuan Xie
Summary: The article introduces an optimal reset technique to continue monitoring after a violation event in online monitoring. By detecting the end of a violation event in real time and skipping the event, it can continue to monitor possible future violation events.
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS
(2022)
Article
Automation & Control Systems
Gang Chen, Peng Wei, Mei Liu
Summary: This article presents a method for constructing a fault detector using signal temporal logic (STL) formulas for a class of switched nonlinear systems with partially unknown dynamics. The method utilizes a Gaussian process for approximating unknown internal dynamics, and a temporal logic inference algorithm for finding the fault detector with stability guarantees. Simulation results demonstrate that the proposed method can detect faulty trajectories with a probability guarantee.
IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING
(2022)
Article
Automation & Control Systems
Chengqian Zhou, Jun Yang, Shihua Li, Wen-Hua Chen
Summary: This article focuses on the robust temporal logic motion control problem for a class of disturbed systems. A disturbance observer (DOB) is used for unmatched disturbance estimation, and signal temporal logic (STL) formulas are introduced to express complex sequential tasks. By utilizing the transient characteristics of the prescribed performance function and the DOB, a continuous feedback composite controller is constructed to maximize robustness. A suitable switched control strategy is presented to guarantee the satisfaction of STL specifications. Experimental results verify the effectiveness of the proposed method.
IEEE TRANSACTIONS ON INDUSTRIAL ELECTRONICS
(2023)
Article
Automation & Control Systems
Lars Lindemann, George J. Pappas, Dimos Dimarogonas
Summary: In this paper, we propose reactive risk signal interval temporal logic (ReRiSITL) for formulating complex spatiotemporal specifications and provide an algorithm to check its satisfiability. We also propose a reactive planning and control framework for dynamical control systems under ReRiSITL specifications.
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
(2022)
Article
Automation & Control Systems
Lars Lindemann, Jakub Nowak, Lukas Schonbachler, Meng Guo, Jana Tumova, Dimos Dimarogonas
Summary: This paper presents the implementation and experimental results of two frameworks for multi-agent systems under temporal logic tasks, where each agent is subject to either a local LTL or STL task and tasks may be coupled. The experimental results include three scenarios demonstrating a variety of tasks.
IEEE TRANSACTIONS ON CONTROL SYSTEMS TECHNOLOGY
(2021)
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
Multidisciplinary Sciences
Brad Wilson, Paulo Rita, Andres Barrios, Bastian Popp
Summary: This study examines how different dimensions of service value in surf camps affect customers' satisfaction and behavioral intentions, finding that various value dimensions have distinct impacts on perceived value, satisfaction, and repurchase intentions.
Article
Automation & Control Systems
Ali Salamati, Sadegh Soudjani, Majid Zamani
Summary: This paper investigates the formal verification of linear time-invariant systems with a partial knowledge of the model, using probabilistic measures, Bayesian inference, and signal temporal logic formulae. The approach combines data-driven and model-based techniques to have a two-layer probabilistic reasoning over the behavior of the system, considering uncertainties in dynamics and observed data in the inner layer, and parameter space distribution in the outer layer. The proposed approach is demonstrated in two case studies.
Article
Chemistry, Analytical
Piotr Kosiuczenko
Summary: Understanding sensor behavior and specifications is complex, with variables such as application domain, sensor usage, and architectures. Various models and technologies have been developed to address this, including a new interval logic called Duration Calculus for Functions (DC4F), which precisely specifies signals from sensors used in heart rhythm monitoring. DC4F is an extension of Duration Calculus, suitable for describing complex interval-dependent behaviors and allows for the specification of desired behavior. This is advantageous over machine learning algorithms, as it allows for hypothesis formulation and user-specified behavior.
Article
Computer Science, Hardware & Architecture
Georgios Tzimpragos, Jennifer Volk, Dilip Vasudevan, Nestan Tsiskaridze, George Michelogiannakis, Advait Madhavan, John Shalf, Timothy Sherwood
Summary: As we approach the end of CMOS transistor scaling, it is necessary to explore novel computing methods to meet the growing demands. The intersection of superconductor electronics and delay-coded computation could provide a more efficient foundation for computing.
Article
History & Philosophy Of Science
Mina Young Pedersen, Marija Slavkovik, Sonja Smets
Summary: Social bots are computer programs that mimic human users on social media platforms, and their detection is mainly done using machine learning approaches. This paper proposes a complementary method of bot detection using model checking, introducing Temporal Network Logic (TNL) to specify social networks and formalize different types of bot behaviors. The paper also explores an extension of the logic using hybrid logic elements. Model checking algorithms for both TNL and its hybrid extension are provided, with the former having complexity in p and the latter in PSPACE.
Article
Multidisciplinary Sciences
Matej Trojak, David Safranek, Lukrecia Mertova, Lubos Brim
Article
Mathematics
Lubos Brim, Samuel Pastva, David Safranek, Eva Smijakova
Summary: Boolean networks are used to study complex dynamic behavior of biological systems, but controlling problems for parameterized Boolean networks have not been addressed yet. The goal of control is to stabilize the system with minimal interventions, and we propose a novel semi-symbolic algorithm to solve this problem efficiently.
Review
Biotechnology & Applied Microbiology
Stanislav Obruca, Pavel Dvorak, Petr Sedlacek, Martin Koller, Karel Sedlar, Iva Pernicova, David Safranek
Summary: This review summarizes the current knowledge on PHA accumulation in halophiles and thermophiles, highlighting the advantages of utilizing extremophiles for PHA production. It also discusses recent advances and future perspectives in metabolic engineering and synthetic biology for improving PHA production. The findings and ideas presented in this review suggest that biotechnological production of PHA by extremophiles can be sustainable and economically feasible, enabling PHA to compete with non-biodegradable petrochemical polymers in the market.
BIOTECHNOLOGY ADVANCES
(2022)
Article
Biochemical Research Methods
Nikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva, David Safranek
Summary: This paper proposes a methodology for analyzing bifurcations in asynchronous parameterized Boolean networks and develops an interactive presentation technique based on decision trees to quickly uncover key parameters affecting changes in attractor landscape. The method is applied to the study of complex cell signaling networks and yields results consistent with recent biological findings.
BMC BIOINFORMATICS
(2022)
Article
Computer Science, Theory & Methods
Nikola Benes, Lubos Brim, Samuel Pastva, David Safranek
Summary: Edge-coloured directed graphs are essential for modelling and analyzing complex systems in various scientific disciplines. This paper proposes a novel algorithm that symbolically computes all the monochromatic strongly connected components of an edge-coloured graph. The algorithm is evaluated using an experimental implementation based on binary decision diagrams (BDDs), and its effectiveness is demonstrated.
LOGICAL METHODS IN COMPUTER SCIENCE
(2022)
Article
Biochemical Research Methods
Nikola Benes, Lubos Brim, Ondrej Huvar, Samuel Pastva, David Safranek, Eva Smijakova
Summary: AEON.py is a Python library used for analyzing the long-term behavior of very large asynchronous Boolean networks. It offers significant computational improvements over existing methods for attractor detection and can analyze partially specified networks with uncertain update functions. It also includes techniques for identifying viable source-target control strategies and evaluating their robustness with parameter perturbations.
Article
Biology
Lubos Brim, Samuel Pastva, David Safranek, Eva Smijakova
Summary: Boolean networks are widely used in computational systems biology for modeling. However, it is often challenging to find a single Boolean network that matches biological reality perfectly. This paper introduces partially specified Boolean networks (PSBNs) to represent the uncertainty in the model and proposes a symbolic methodology for controlling PSBNs. The efficiency of perturbations in PSBNs is evaluated using the perturbation robustness metric. Experimental results show that one-step perturbations in PSBNs are less robust compared to temporary and permanent perturbations.
Article
Biochemical Research Methods
Tatjana Petrov, Matej Hajnal, Julia Klein, David Safranek, Morgane Nouvian
Summary: Honeybees protect their colony by mass stinging and coordinate their actions through alarm pheromone. Understanding how individual bees adapt their stinging response during an attack is a challenge. The researchers observed the behavior of bee groups confronted with a fake predator and proposed a model that links individual bee choices to the group context. They also developed a method to infer the model parameters and found that group size affects stinging initiation and alarm pheromone recruitment.
PLOS COMPUTATIONAL BIOLOGY
(2022)
Article
Biology
Matej Trojak, David Safranek, Samuel Pastva, Lubos Brim
Summary: In systems biology, models are essential in understanding systems being studied. Among various modelling approaches, rewriting systems offer a framework for mechanistic level system description. Describing biochemical processes often involves incorporating abstract knowledge to simplify the system or compensate for missing details. To address this, we propose regulation mechanisms as an extension of this formalism, introducing additional controls on the rewriting process. We demonstrate the application of these mechanisms in a rule-based language suitable for modeling biological phenomena and present case studies from the biochemical domain.
Proceedings Paper
Computer Science, Theory & Methods
Matej Hajnal, David Safranek, Tatjana Petrov
Summary: The tool presented combines existing methods for parameter synthesis of Discrete-time Markov chains, with several hybrid methods for parameter space exploration. Users can choose between different parameter exploration methods based on trade-offs between scalability and inference quality. Its performance has been evaluated on several benchmarks.
PERFORMANCE ENGINEERING AND STOCHASTIC MODELING
(2021)
Proceedings Paper
Computer Science, Hardware & Architecture
Nikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva, David Safranek
COMPUTER AIDED VERIFICATION (CAV 2020), PT I
(2020)
Article
Mathematics, Interdisciplinary Applications
Nikola Benes, Lubos Brim, Samuel Pastva, David Safranek
INTERNATIONAL JOURNAL OF BIFURCATION AND CHAOS
(2020)
Proceedings Paper
Computer Science, Theory & Methods
Matej Trojak, David Safranek, Lubos Brim, Jakub Salagovic, Jan Cerveny
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
(2020)
Article
Computer Science, Theory & Methods
Isaac Mackey, Raghubir Chimni, Jianwen Su
Summary: Software systems rely on events for various purposes, and monitoring event streams can ensure compliance with policies. This paper aims to develop techniques for early detection of time constraint violations and presents experimental results to demonstrate the feasibility and benefits of the approach.
INFORMATION AND COMPUTATION
(2024)
Article
Computer Science, Theory & Methods
Girish Balakrishnan, Sankardeep Chakraborty, N. S. Narayanaswamy, Kunihiko Sadakane
Summary: This paper addresses the problem of designing a succinct data structure for path graphs and provides two solutions. The first solution supports adjacency, neighbourhood, and degree queries with time complexities of O(log n), O(d log n), and min{O(log2 n), O(d log n)} respectively. The second solution is a space-efficient data structure that optimally supports adjacency, neighbourhood, and degree queries.
INFORMATION AND COMPUTATION
(2024)
