Neural Network for Weighted Signal Temporal Logic

In this paper, we propose a neuro-symbolic framework called weighted Signal Temporal Logic Neural Network (wSTL-NN) that combines the characteristics of neural networks and temporal logics. Weighted Signal Temporal Logic (wSTL) formulas are recursively composed of subformulas that are combined using logical and temporal operators. The quantitative semantics of wSTL is defined such that the quantitative satisfaction of subformulas with higher weights has more influence on the quantitative satisfaction of the overall wSTL formula. In the wSTL-NN, each neuron corresponds to a wSTL subformula, and its output corresponds to the quantitative satisfaction of the formula. We use wSTL-NN to represent wSTL formulas as features to classify time series data. STL features are more explainable than those used in classical methods. The wSTL-NN is end-to-end differentiable, which allows learning of wSTL formulas to be done using back-propagation. To reduce the number of weights, we introduce two techniques to sparsify the wSTL-NN.We apply our framework to an occupancy detection time-series dataset to learn a classifier that predicts the occupancy status of an office room.

Distributed Monitoring of Robot Swarms with Swarm Signal Temporal Logic

In this paper, we develop a distributed monitoring framework for robot swarms so that the agents can monitor whether the executions of robot swarms satisfy Swarm Signal Temporal Logic (SwarmSTL) formulas. We define generalized moments (GMs) to represent swarm features. A dynamic generalized moments consensus algorithm (GMCA) with Kalman filter (KF) is proposed so that each agent can estimate the GMs. Also, we obtain an upper bound for the error between an agents estimate and the actual GMs. This bound is independent of the motion of the agents. We also propose rules for monitoring SwarmSTL temporal and logical operators. As a result, the agents can monitor whether the swarm satisfies SwarmSTL formulas with a certain confidence level using these rules and the bound of the estimation error. The distributed monitoring framework is applied to a swarm transporting supplies example, where we also show the efficacy of the Kalman filter in the dynamic generalized moments consensus process.

Temporal Logic Inference for Hybrid System Observation with Spatial and Temporal Uncertainties

In this paper, we present a mechanism for building hybrid system observers to differentiate between specific positions of the hybrid system. The mechanism is designed through inferring metric temporal logic (MTL) formulae from simulated trajectories from the hybrid system. We first approximate the system behavior by simulating finitely many trajectories with timerobust tube segments around them. These time-robust tube segments account for both spatial and temporal uncertainties that exist in the hybrid system with initial state variations. The inferred MTL formulae classify different time-robust tube segments and thus can be used for classifying the hybrid system behaviors in a provably correct fashion. We implement our approach on a model of a smart building testbed to distinguish two cases of room occupancy.

Controller Synthesis of Wind Turbine Generator and Energy Storage System with Stochastic Wind Variations under Temporal Logic Specifications

In this paper, we present a controller synthesis approach for wind turbine generators (WTG) and energy storage systems with metric temporal logic (MTL) specifications, with provable probabilistic guarantees in the stochastic environment of wind power generation. The MTL specifications are requirements for the grid frequency deviations, WTG rotor speed variations and the power flow constraints at different lines. We present the stochastic control bisimulation function, which bounds the divergence of the trajectories of a switched stochastic control system and the switched nominal control system in a probabilistic fashion.We first design a feedforward controller by solving an optimization problem for the nominal trajectory of the deterministic control system with robustness against initial state variations and stochastic uncertainties. Then we generate a feedback control law from the data of the simulated trajectories. We implement our control method on both a four-bus system and a nine-bus system, and test the effectiveness of the method with a generation loss disturbance. We also test the advantage of the feedback controller over the feedforward controller when unexpected disturbance occurs.

Graph Temporal Logic Inference for Classification and Identification

Inferring spatial-temporal properties from data is important for many complex systems, such as additive manufacturing systems, swarm robotic systems and biological networks. Such systems can often be modeled as a labeled graph where labels on the nodes and edges represent relevant measurements such as temperatures and distances. We introduce graph temporal logic (GTL) which can express properties such as whenever a nodes label is above 10, for the next 3 time units there are always at least two neighboring nodes with an edge label of at most 2 where the node labels are above 5. This paper is a first attempt to infer spatial (graph) temporal logic formulas from data for classification and identification. For classification, we infer a GTL formula that classifies two sets of graph temporal trajectories with minimal misclassification rate. For identification, we infer a GTL formula that is informative and is satisfied by the graph temporal trajectories in the dataset with high probability. The informativeness of a GTL formula is measured by the information gain with respect to given prior knowledge represented by a prior probability distribution. We implement the proposed approach to classify the graph patterns of tensile specimens built from selective laser sintering (SLS) process with varying strengths, and to identify informative spatial-temporal patterns from experimental data of the SLS cooldown process and simulation data of a swarm of robots.

Rapid Circadian Entrainment in Models of Circadian Genes Regulation

The light-based minimum-time circadian entrainment problem for mammals, Neurospora, and Drosophila is studied based on the mathematical models of their circadian gene regulation. These models contain high order nonlinear differential equations. Two model simplification methods are applied to these high-order models: the phase response curves (PRC) and the Principal Orthogonal Decomposition (POD). The variational calculus and a gradient descent algorithm are applied for solving the optimal light input in the high-order models. As the results of the gradient descent algorithm rely heavily on the initial guesses, we use the optimal control of the PRC and the simplified model to initialize the gradient descent algorithm. In this paper, we present: (1) the application of PRC and direct shooting algorithm on high-order nonlinear models; (2) a general process for solving the minimum-time optimal control problem on high-order models; (3) the impacts of minimum-time optimal light on circadian gene transcription and protein synthesis.

Information-Guided Temporal Logic Inference with Prior Knowledge

This paper investigates the problem of inferring knowledge from data so that the inferred knowledge is interpretable and informative to humans who have prior knowledge. Given a dataset as a collection of system trajectories, we infer parametric linear temporal logic (pLTL) formulas that are informative and satisfied by the trajectories in the dataset with high probability. The informativeness of the inferred formula is measured by the information gain with respect to given prior knowledge represented by a prior probability distribution. We first present two algorithms to compute the information gain with a focus on two types of prior probability distributions: stationary probability distributions and probability distributions expressed by discrete time Markov chains. Then we provide a method to solve the inference problem for a subset of pLTL formulas with polynomial time complexity with respect to the number of Boolean connectives in the formula. We provide implementations of the proposed approach on explaining anomalous patterns, patterns changes and explaining the policies of Markov decision processes.

Continuous Circadian Phase Estimation Using Adaptive Notch Filter

Actigraphy has been widely used for the analysis of circadian rhythm. Current practice applies regression analysis to data from multiple days to estimate the circadian phase. This paper presents a filtering method for online processing of biometric data to estimate the circadian phase. We apply the proposed method on actigraphy data of fruit flies (Drosophila melanogaster).

Census Signal Temporal Logic Inference for Multi-Agent Group Behavior Analysis

In this paper, we define a novel census signal temporal logic (CensusSTL) that focuses on the number of agents in different subsets of a group that complete a certain task specified by the signal temporal logic (STL). CensusSTL consists of an inner logic STL formula and an outer logic STL formula. We present a new inference algorithm to infer CensusSTL formulae from the trajectory data of a group of agents. We first identify the inner logic STL formula and then infer the subgroups based on whether the agents behaviors satisfy the inner logic formula at each time point. We use two different approaches to infer the subgroups based on similarity and complementarity, respectively. The outer logic CensusSTL formula is inferred from the census trajectories of different subgroups. We apply the algorithm in analyzing data from a soccer match by inferring the CensusSTL formula for different subgroups of a soccer team.