Showing 1–16 of 16 results for author: Hasuo, I

Winning Strategy Templates for Stochastic Parity Games towards Permissive and Resilient Control

Authors: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo

Abstract: Stochastic games play an important role for many purposes such as the control of cyber-physical systems (CPS), where the controller and the environment are modeled as players. Conventional algorithms typically solve the game for a single winning strategy in order to develop a controller. However, in applications such as CPS control, permissive controllers are crucial as they allow the controlled s… ▽ More Stochastic games play an important role for many purposes such as the control of cyber-physical systems (CPS), where the controller and the environment are modeled as players. Conventional algorithms typically solve the game for a single winning strategy in order to develop a controller. However, in applications such as CPS control, permissive controllers are crucial as they allow the controlled system to adapt if additional constraints need to be imposed and also remain resilient to system changes at runtime. In this work, we generalize the concept of permissive winning strategy templates, introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to encompass stochastic games. These templates represent an infinite number of winning strategies and can adapt strategies to system changes efficiently. We focus on five key winning objectives -- safety, reachability, Büchi, co-Büchi, and parity -- and present algorithms to construct templates for each objective. In addition, we propose a novel method to extract a winning strategy from a template and provide discussions on template comparison. △ Less

Submitted 13 September, 2024; originally announced September 2024.

Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications

Authors: Sota Sato, Jie An, Zhenya Zhang, Ichiro Hasuo

Abstract: We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encoding of the STL semantics; it follows the idea of stable partitioning from the recent work on SMT-based STL model checking. Assuming that our (continuous-time) system models can be encoded to MILP -- typical examples are… ▽ More We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encoding of the STL semantics; it follows the idea of stable partitioning from the recent work on SMT-based STL model checking. Assuming that our (continuous-time) system models can be encoded to MILP -- typical examples are rectangular hybrid automata (precisely) and hybrid dynamics with closed-form solutions (approximately) -- our MILP encoding yields an optimization-based model checking algorithm that is scalable, is anytime/interruptible, and accommodates parameter mining. Experimental evaluation shows our algorithm's performance advantages especially for complex STL formulas, demonstrating its practical relevance e.g. in the automotive domain. △ Less

Submitted 13 August, 2024; originally announced August 2024.

Comments: Extended version of the paper accepted by 36th International Conference on Computer-Aided Verification (CAV), 2024

Online Causation Monitoring of Signal Temporal Logic

Authors: Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo

Abstract: Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL). The classic STL monitoring is performed by computing a robustness interval that specifies, at each instant, how far the monitored signals are from violating and satisfying the specification. Howev… ▽ More Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of a system satisfy a specification in, e.g., Signal Temporal Logic (STL). The classic STL monitoring is performed by computing a robustness interval that specifies, at each instant, how far the monitored signals are from violating and satisfying the specification. However, since a robustness interval monotonically shrinks during monitoring, classic online monitors may fail in reporting new violations or in precisely describing the system evolution at the current instant. In this paper, we tackle these issues by considering the causation of violation or satisfaction, instead of directly using the robustness. We first introduce a Boolean causation monitor that decides whether each instant is relevant to the violation or satisfaction of the specification. We then extend this monitor to a quantitative causation monitor that tells how far an instant is from being relevant to the violation or satisfaction. We further show that classic monitors can be derived from our proposed ones. Experimental results show that the two proposed monitors are able to provide more detailed information about system evolution, without requiring a significantly higher monitoring cost. △ Less

Submitted 28 May, 2023; originally announced May 2023.

Comments: 31 pages, 7 figures, the full version of the paper accepted by CAV 2023

Model-bounded monitoring of hybrid systems

Authors: Masaki Waga, Étienne André, Ichiro Hasuo

Abstract: Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target sys… ▽ More Monitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs) -- the LHAs are called bounding models. We introduce a novel notion of monitored language of LHAs, and we reduce the monitoring problem to the membership problem of the monitored language. We present two partial algorithms -- one is via reduction to reachability in LHAs and the other is a direct one using polyhedra -- and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant. △ Less

Submitted 25 July, 2024; v1 submitted 15 February, 2021; originally announced February 2021.

Comments: This is the author version of the manuscript of the same name published in the ACM Transactions on Cyber-Physical Systems

ACM Class: D.2.4; F.3.1

Journal ref: ACM Transactions on Cyber-Physical Systems, Volume 6, Issue 4, Article No.: 30, Pages 1-26, 2022

Constrained Optimization for Hybrid System Falsification and Application to Conjunctive Synthesis

Authors: Sota Sato, Masaki Waga, Ichiro Hasuo

Abstract: The synthesis problem of a cyber-physical system (CPS) is to find an input signal under which the system's behavior satisfies a given specification. Our setting is that the specification is a formula of signal temporal logic, and furthermore, that the specification is a conjunction of different and often conflicting requirements. Conjunctive specifications are often challenging for optimization-ba… ▽ More The synthesis problem of a cyber-physical system (CPS) is to find an input signal under which the system's behavior satisfies a given specification. Our setting is that the specification is a formula of signal temporal logic, and furthermore, that the specification is a conjunction of different and often conflicting requirements. Conjunctive specifications are often challenging for optimization-based falsification -- an established method for CPS analysis that can also be used for synthesis -- since the usual framework (especially how its robust semantics handles Boolean connectives) is not suited for finding delicate trade-offs between different requirements. Our proposed method consists of the combination of optimization-based falsification and constrained optimization. Specifically, we show that the state-of-the-art multiple constraint ranking method can be combined with falsification powered by CMA-ES optimization; its performance advantage is demonstrated in experiments. △ Less

Submitted 9 February, 2021; v1 submitted 1 December, 2020; originally announced December 2020.

Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches

Authors: Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo

Abstract: Falsification of hybrid systems is attracting ever-growing attention in quality assurance of Cyber-Physical Systems (CPS) as a practical alternative to exhaustive formal verification. In falsification, one searches for a falsifying input that drives a given black-box model to output an undesired signal. In this paper, we identify input constraints---such as the constraint "the throttle and brake p… ▽ More Falsification of hybrid systems is attracting ever-growing attention in quality assurance of Cyber-Physical Systems (CPS) as a practical alternative to exhaustive formal verification. In falsification, one searches for a falsifying input that drives a given black-box model to output an undesired signal. In this paper, we identify input constraints---such as the constraint "the throttle and brake pedals should not pressed simultaneously" for an automotive powertrain model---as a key factor for the practical value of falsification methods. We propose three approaches for systematically addressing input constraints in optimization-based falsification, two among which come from the lexicographic method studied in the context of constrained multi-objective optimization. Our experiments show the approaches' effectiveness. △ Less

Submitted 13 April, 2020; v1 submitted 14 January, 2020; originally announced January 2020.

Comments: Accepted by 12th NASA Formal Methods Symposium (NFM 2020)

Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification (Extended Version)

Authors: Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini

Abstract: Hybrid system falsification is an actively studied topic, as a scalable quality assurance methodology for real-world cyber-physical systems. In falsification, one employs stochastic hill-climbing optimization to quickly find a counterexample input to a black-box system model. Quantitative robust semantics is the technical key that enables use of such optimization. In this paper, we tackle the so-c… ▽ More Hybrid system falsification is an actively studied topic, as a scalable quality assurance methodology for real-world cyber-physical systems. In falsification, one employs stochastic hill-climbing optimization to quickly find a counterexample input to a black-box system model. Quantitative robust semantics is the technical key that enables use of such optimization. In this paper, we tackle the so-called scale problem regarding Boolean connectives that is widely recognized in the community: quantities of different scales (such as speed [km/h] vs. RPM, or worse, RPH) can mask each other's contribution to robustness. Our solution consists of integration of the multi-armed bandit algorithms in hill climbing-guided falsification frameworks, with a technical novelty of a new reward notion that we call hill-climbing gain. Our experiments show our approach's robustness under the change of scales, and that it outperforms a state-of-the-art falsification tool. △ Less

Submitted 23 June, 2019; v1 submitted 18 May, 2019; originally announced May 2019.

Comments: CAV 2019

Symbolic Monitoring against Specifications Parametric in Time and Data

Authors: Masaki Waga, Étienne André, Ichiro Hasuo

Abstract: Monitoring consists in deciding whether a log meets a given specification. In this work, we propose an automata-based formalism to monitor logs in the form of actions associated with time stamps and arbitrarily data values over infinite domains. Our formalism uses both timing parameters and data parameters, and is able to output answers symbolic in these parameters and in the log segments where th… ▽ More Monitoring consists in deciding whether a log meets a given specification. In this work, we propose an automata-based formalism to monitor logs in the form of actions associated with time stamps and arbitrarily data values over infinite domains. Our formalism uses both timing parameters and data parameters, and is able to output answers symbolic in these parameters and in the log segments where the property is satisfied or violated. We implemented our approach in an ad-hoc prototype SyMon, and experiments show that its high expressive power still allows for efficient online monitoring. △ Less

Submitted 11 May, 2019; originally announced May 2019.

Comments: Accepted to CAV 2019

Offline timed pattern matching under uncertainty

Authors: Étienne André, Ichiro Hasuo, Masaki Waga

Abstract: Given a log and a specification, timed pattern matching aims at exhibiting for which start and end dates a specification holds on that log. For example, "a given action is always followed by another action before a given deadline". This problem has strong connections with monitoring real-time systems. We address here timed pattern matching in presence of an uncertain specification, i.e., that may… ▽ More Given a log and a specification, timed pattern matching aims at exhibiting for which start and end dates a specification holds on that log. For example, "a given action is always followed by another action before a given deadline". This problem has strong connections with monitoring real-time systems. We address here timed pattern matching in presence of an uncertain specification, i.e., that may contain timing parameters (e.g., the deadline can be uncertain or unknown). That is, we want to know for which start and end dates, and for what values of the deadline, this property holds. Or what is the minimum or maximum deadline (together with the corresponding start and end dates) for which this property holds. We propose here a framework for timed pattern matching based on parametric timed model checking. In contrast to most parametric timed problems, the solution is effectively computable, and we perform experiments using IMITATOR to show the applicability of our approach. △ Less

Submitted 20 December, 2018; originally announced December 2018.

ACM Class: F.4

Journal ref: ICECCS 2018, IEEE CPS, pages 10-20, December 2018. Best paper award

Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input

Authors: Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo

Abstract: We present an algorithm that quickly finds falsifying inputs for hybrid systems, i.e., inputs that steer the system towards violation of a given temporal logic requirement. Our method is based on a probabilistically directed search of an increasingly fine grained spatial and temporal discretization of the input space. A key feature is that it adapts to the difficulty of a problem at hand, specific… ▽ More We present an algorithm that quickly finds falsifying inputs for hybrid systems, i.e., inputs that steer the system towards violation of a given temporal logic requirement. Our method is based on a probabilistically directed search of an increasingly fine grained spatial and temporal discretization of the input space. A key feature is that it adapts to the difficulty of a problem at hand, specifically to the local complexity of each input segment, as needed for falsification. In experiments with standard benchmarks, our approach consistently outperforms existing techniques by a significant margin. In recognition of the way it works and to distinguish it from previous work, we describe our method as a "Las Vegas tree search". △ Less

Submitted 10 December, 2018; originally announced December 2018.

Two-Layered Falsification of Hybrid Systems guided by Monte Carlo Tree Search

Authors: Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, Ichiro Hasuo

Abstract: Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification---a methodology of search-based testing that employs stochastic optimization---is attracting attention as an alternative quality assurance method. Inspired by the recent works that advocate coverage and exploration in falsification, we introduce a tw… ▽ More Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification---a methodology of search-based testing that employs stochastic optimization---is attracting attention as an alternative quality assurance method. Inspired by the recent works that advocate coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations. MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. △ Less

Submitted 12 August, 2018; v1 submitted 16 March, 2018; originally announced March 2018.

Time-Staging Enhancement of Hybrid System Falsification

Authors: Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, Sean Sedwards

Abstract: Optimization-based falsification employs stochastic optimization algorithms to search for error input of hybrid systems. In this paper we introduce a simple idea to enhance falsification, namely time staging, that allows the time-causal structure of time-dependent signals to be exploited by the optimizers. Time staging consists of running a falsification solver multiple times, from one interval to… ▽ More Optimization-based falsification employs stochastic optimization algorithms to search for error input of hybrid systems. In this paper we introduce a simple idea to enhance falsification, namely time staging, that allows the time-causal structure of time-dependent signals to be exploited by the optimizers. Time staging consists of running a falsification solver multiple times, from one interval to another, incrementally constructing an input signal candidate. Our experiments show that time staging can dramatically increase performance in some realistic examples. We also present theoretical results that suggest the kinds of models and specifications for which time staging is likely to be effective. △ Less

Submitted 14 July, 2022; v1 submitted 10 March, 2018; originally announced March 2018.

Comments: In Proceedings SNR 2021, arXiv:2207.04391

Journal ref: EPTCS 361, 2022, pp. 25-43

Bounding Errors Due to Switching Delays in Incrementally Stable Switched Systems (Extended Version)

Authors: Kengo Kido, Sean Sedwards, Ichiro Hasuo

Abstract: Time delays pose an important challenge in networked control systems, which are now ubiquitous. Focusing on switched systems, we introduce a framework that provides an upper bound for errors caused by switching delays. Our framework is based on approximate bisimulation, a notion that has been previously utilized mainly for symbolic (discrete) abstraction of state spaces. Notable in our framework i… ▽ More Time delays pose an important challenge in networked control systems, which are now ubiquitous. Focusing on switched systems, we introduce a framework that provides an upper bound for errors caused by switching delays. Our framework is based on approximate bisimulation, a notion that has been previously utilized mainly for symbolic (discrete) abstraction of state spaces. Notable in our framework is that, in deriving an approximate bisimulation and thus an error bound, we use a simple incremental stability assumption (namely δ-GUAS) that does not itself refer to time delays. That this is the same assumption used for state-space discretization enables a two-step workflow for control synthesis for switched systems, in which a single Lyapunov-type stability witness serves for two different purposes of state discretization and coping with time delays. We demonstrate the proposed framework with a boost DC-DC converter, a common example of switched systems. △ Less

Submitted 23 December, 2017; v1 submitted 18 December, 2017; originally announced December 2017.

Causality-Aided Falsification

Authors: Takumi Akazaki, Yoshihiro Kumazawa, Ichiro Hasuo

Abstract: Falsification is drawing attention in quality assurance of heterogeneous systems whose complexities are beyond most verification techniques' scalability. In this paper we introduce the idea of causality aid in falsification: by providing a falsification solver -- that relies on stochastic optimization of a certain cost function -- with suitable causal information expressed by a Bayesian network, s… ▽ More Falsification is drawing attention in quality assurance of heterogeneous systems whose complexities are beyond most verification techniques' scalability. In this paper we introduce the idea of causality aid in falsification: by providing a falsification solver -- that relies on stochastic optimization of a certain cost function -- with suitable causal information expressed by a Bayesian network, search for a falsifying input value can be efficient. Our experiment results show the idea's viability. △ Less

Submitted 8 September, 2017; originally announced September 2017.

Comments: In Proceedings FVAV 2017, arXiv:1709.02126

Journal ref: EPTCS 257, 2017, pp. 3-18

Time Robustness in MTL and Expressivity in Hybrid System Falsification (Extended Version)

Authors: Takumi Akazaki, Ichiro Hasuo

Abstract: Building on the work by Fainekos and Pappas and the one by Donze and Maler, we introduce AvSTL, an extension of metric interval temporal logic by averaged temporal operators. Its expressivity in capturing both space and time robustness helps solving falsification problems, (i.e. searching for a critical path in hybrid system models); it does so by communicating a designer's intention more faithful… ▽ More Building on the work by Fainekos and Pappas and the one by Donze and Maler, we introduce AvSTL, an extension of metric interval temporal logic by averaged temporal operators. Its expressivity in capturing both space and time robustness helps solving falsification problems, (i.e. searching for a critical path in hybrid system models); it does so by communicating a designer's intention more faithfully to the stochastic optimization engine employed in a falsification solver. We also introduce a sliding window-like algorithm that keeps the cost of computing truth/robustness values tractable. △ Less

Submitted 27 May, 2015; v1 submitted 23 May, 2015; originally announced May 2015.

Comments: 22pages, a long version of the paper accepted in 27th International Conference on Computer Aided Verification (CAV 2015)

Input Synthesis for Sampled Data Systems by Program Logic

Authors: Takumi Akazaki, Ichiro Hasuo, Kohei Suenaga

Abstract: Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturbance or noise), find an input sequence that steers the system to the desired postcondition. In this paper we focus on sampled data systems--systems in which a digital controller interrupts a physical plant in a periodi… ▽ More Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturbance or noise), find an input sequence that steers the system to the desired postcondition. In this paper we focus on sampled data systems--systems in which a digital controller interrupts a physical plant in a periodic manner, a class commonly known in control theory--and furthermore assume that a controller is given in the form of an imperative program. We develop a structural approach to input synthesis that features forward and backward reasoning in program logic for the purpose of reducing a search space. Although the examples we cover are limited both in size and in structure, experiments with a prototype implementation suggest potential of our program logic based approach. △ Less

Submitted 24 January, 2015; originally announced January 2015.

Comments: In Proceedings HAS 2014, arXiv:1501.05405

Journal ref: EPTCS 174, 2015, pp. 22-39