More Like this

1. Strategy synthesis for partially-known switched stochastic systems

   https://doi.org/10.1145/3447928.3456649  

   Jackson, John; Laurenti, Luca; Frew, Eric; Lahijanian, Morteza (May 2021, The 24th International Conference on Hybrid Systems: Computation and Control)

   null (Ed.)

   We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertainty in the learning step. Then, we synthesize a strategy on the resulting IMDP that maximizes the satisfaction probability of the LTLf specification and is robust against all the uncertainties in the abstraction. This strategy is then refined into a switching strategy for the original stochastic system. We show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal strategy. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems. 

   more » « less
2. Detecting disturbances in network-coupled dynamical systems with machine learning

   https://doi.org/10.1063/5.0169237  

   Skardal, Per Sebastian; Restrepo, Juan G (October 2023, Chaos: An Interdisciplinary Journal of Nonlinear Science)

   Identifying disturbances in network-coupled dynamical systems without knowledge of the disturbances or underlying dynamics is a problem with a wide range of applications. For example, one might want to know which nodes in the network are being disturbed and identify the type of disturbance. Here, we present a model-free method based on machine learning to identify such unknown disturbances based only on prior observations of the system when forced by a known training function. We find that this method is able to identify the locations and properties of many different types of unknown disturbances using a variety of known forcing functions. We illustrate our results with both linear and nonlinear disturbances using food web and neuronal activity models. Finally, we discuss how to scale our method to large networks. 

   more » « less
3. LTLf Synthesis under Partial Observability: From Theory to Practice

   https://doi.org/10.4204/EPTCS.326.1  

   Tabajara, Lucas M; Vardi, Moshe Y (October 2020, The Eleventh International Symposium on Games, Automata, Logics, and Formal Verification (GandALF))

   LTL synthesis is the problem of synthesizing a reactive system from a formal specification in Linear Temporal Logic. The extension of allowing for partial observability, where the system does not have direct access to all relevant information about the environment, allows generalizing this problem to a wider set of real-world applications, but the difficulty of implementing such an extension in practice means that it has remained in the realm of theory. Recently, it has been demonstrated that restricting LTL synthesis to systems with finite executions by using LTL with finite-horizon semantics (LTLf) allows for significantly simpler implementations in practice. With the conceptual simplicity of LTLf, it becomes possible to explore extensions such as partial observability in practice for the first time. Previous work has analyzed the problem of LTLf synthesis under partial observability theoretically and suggested two possible algorithms, one with 3EXPTIME and another with 2EXPTIME complexity. In this work, we first prove a complexity lower bound conjectured in earlier work. Then, we complement the theoretical analysis by showing how the two algorithms can be integrated in practice into an established framework for LTLf synthesis. We furthermore identify a third, MSO-based, approach enabled by this framework. Our experimental evaluation reveals very different results from what the theory seems to suggest, with the 3EXPTIME algorithm often outperforming the 2EXPTIME approach. Furthermore, as long as it is able to overcome an initial memory bottleneck, the MSO-based approach can often outperforms the others. 

   more » « less
4. LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work

   https://doi.org/10.24963/ijcai.2022/359  

   De Giacomo, Giuseppe; Favorito, Marco; Li, Jianwen; Vardi, Moshe Y.; Xiao, Shengping; Zhu, Shufang (July 2022, IJCAI)

   Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this paper, we develop a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently. 

   more » « less
5. High-order strongly nonlinear long wave approximation and solitary wave solution

   https://doi.org/10.1017/jfm.2022.544  

   Choi, Wooyoung (August 2022, Journal of Fluid Mechanics)

   We consider high-order strongly nonlinear long wave models expanded in a single small parameter measuring the ratio of the water depth to the characteristic wavelength. By examining its dispersion relation, the high-order system for the bottom velocity is found stable to all disturbances at any order of approximation. On the other hand, systems for other velocities can be unstable and even ill-posed, as signified by the unbounded maximum growth. Under the steady assumption, a new third-order solitary wave solution of the Euler equations is obtained using the high-order strongly nonlinear system and is expanded in an amplitude parameter, which is different from that used in weakly nonlinear theory. The third-order solution is shown to well describe various physical quantities induced by a finite-amplitude solitary wave, including the wave profile, horizontal velocity profile, particle velocity at the crest and bottom pressure. For numerical computations, the first- and second-order strongly nonlinear systems for the bottom velocity are considered. It is shown that finite difference schemes are unstable due to truncation errors introduced in approximating high-order spatial derivatives and, therefore, a more accurate spatial discretization scheme is necessary. Using a pseudo-spectral method based on finite Fourier series combined with an iterative scheme for the inversion of a non-local operator, the strongly nonlinear systems are solved numerically for the propagation of a single solitary wave and the head-on collision of two counter-propagating solitary waves of finite amplitudes, and the results are compared with previous laboratory measurements. 

   more » « less