-
Formal Verification of Safety Architectures for Automated Driving
Authors:
Clovis Eberhart,
Jérémy Dubut,
James Haydon,
Ichiro Hasuo
Abstract:
Safety architectures play a crucial role in the safety assurance of automated driving vehicles (ADVs). They can be used as safety envelopes of black-box ADV controllers, and for graceful degradation from one ODD to another. Building on our previous work on the formalization of responsibility-sensitive safety (RSS), we introduce a novel program logic that accommodates assume-guarantee reasoning and…
▽ More
Safety architectures play a crucial role in the safety assurance of automated driving vehicles (ADVs). They can be used as safety envelopes of black-box ADV controllers, and for graceful degradation from one ODD to another. Building on our previous work on the formalization of responsibility-sensitive safety (RSS), we introduce a novel program logic that accommodates assume-guarantee reasoning and fallback-like constructs. This allows us to formally define and prove the safety of existing and novel safety architectures. We apply the logic to a pull over scenario and experimentally evaluate the resulting safety architecture.
△ Less
Submitted 20 August, 2023;
originally announced August 2023.
-
Formal Verification of Intersection Safety for Automated Driving
Authors:
James Haydon,
Martin Bondu,
Clovis Eberhart,
Jérémy Dubut,
Ichiro Hasuo
Abstract:
We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a nove…
▽ More
We build on our recent work on formalization of responsibility-sensitive safety (RSS) and present the first formal framework that enables mathematical proofs of the safety of control strategies in intersection scenarios. Intersection scenarios are challenging due to the complex interaction between vehicles; to cope with it, we extend the program logic dFHL in the previous work and introduce a novel formalism of hybrid control flow graphs on which our algorithm can automatically discover an RSS condition that ensures safety. An RSS condition thus discovered is experimentally evaluated; we observe that it is safe (as our safety proof says) and is not overly conservative.
△ Less
Submitted 13 August, 2023;
originally announced August 2023.
-
Compositional Probabilistic Model Checking with String Diagrams of MDPs
Authors:
Kazuki Watanabe,
Clovis Eberhart,
Kazuyuki Asada,
Ichiro Hasuo
Abstract:
We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evalu…
▽ More
We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages.
△ Less
Submitted 17 July, 2023;
originally announced July 2023.
-
Compositional Solution of Mean Payoff Games by String Diagrams
Authors:
Kazuki Watanabe,
Clovis Eberhart,
Kazuyuki Asada,
Ichiro Hasuo
Abstract:
Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs). The framework is derived from category theory, specifically that of monoidal categories: MPGs (extended with open ends) get composed in so-called string diagrams and thus organized in a monoidal category; their soluti…
▽ More
Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs). The framework is derived from category theory, specifically that of monoidal categories: MPGs (extended with open ends) get composed in so-called string diagrams and thus organized in a monoidal category; their solution is then expressed as a functor, whose preservation properties embody compositionality. As usual, the key question to compositionality is how to enrich the semantic domain; the categorical framework gives an informed guidance in solving the question by singling out the algebraic structure required in the extended semantic domain. We implemented our compositional solution in Haskell; depending on benchmarks, it can outperform an existing algorithm by an order of magnitude.
△ Less
Submitted 16 July, 2023;
originally announced July 2023.
-
Goal-Aware RSS for Complex Scenarios via Program Logic
Authors:
Ichiro Hasuo,
Clovis Eberhart,
James Haydon,
Jérémy Dubut,
Rose Bohrer,
Tsutomu Kobayashi,
Sasinee Pruekprasert,
Xiao-Yi Zhang,
Erik André Pallas,
Akihisa Yamada,
Kohei Suenaga,
Fuyuki Ishikawa,
Kenji Kamijo,
Yoshiyuki Shinya,
Takamasa Suetomi
Abstract:
We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement -- in addition to collision avoidance as in the original RSS -- requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reaso…
▽ More
We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS rules guarantee goal achievement -- in addition to collision avoidance as in the original RSS -- requires complex planning over long sequences of manoeuvres. To deal with the complexity, we introduce a compositional reasoning framework based on program logic, in which one can systematically develop RSS rules for smaller subscenarios and combine them to obtain RSS rules for bigger scenarios. As the basis of the framework, we introduce a program logic dFHL that accommodates continuous dynamics and safety conditions. Our framework presents a dFHL-based workflow for deriving goal-aware RSS rules; we discuss its software support, too. We conducted experimental evaluation using RSS rules in a safety architecture. Its results show that goal-aware RSS is indeed effective in realising both collision avoidance and goal achievement.
△ Less
Submitted 5 July, 2022;
originally announced July 2022.
-
Moment Propagation of Polynomial Systems Through Carleman Linearization for Probabilistic Safety Analysis
Authors:
Sasinee Pruekprasert,
Jérémy Dubut,
Toru Takisaka,
Clovis Eberhart,
Ahmet Cetinkaya
Abstract:
We develop a method to approximate the moments of a discrete-time stochastic polynomial system. Our method is built upon Carleman linearization with truncation. Specifically, we take a stochastic polynomial system with finitely many states and transform it into an infinite-dimensional system with linear deterministic dynamics, which describe the exact evolution of the moments of the original polyn…
▽ More
We develop a method to approximate the moments of a discrete-time stochastic polynomial system. Our method is built upon Carleman linearization with truncation. Specifically, we take a stochastic polynomial system with finitely many states and transform it into an infinite-dimensional system with linear deterministic dynamics, which describe the exact evolution of the moments of the original polynomial system. We then truncate this deterministic system to obtain a finite-dimensional linear system, and use it for moment approximation by iteratively propagating the moments along the finite-dimensional linear dynamics across time. We provide efficient online computation methods for this propagation scheme with several error bounds for the approximation. Our results also show that precise values of certain moments at a given time step can be obtained when the truncated system is sufficiently large. Furthermore, we investigate techniques to reduce the offline computation load using reduced Kronecker power. Based on the obtained approximate moments and their errors, we also provide hyperellipsoidal regions that are safe for some given probability bound. Those bounds allow us to conduct probabilistic safety analysis online through convex optimization. We demonstrate our results on a logistic map with stochastic dynamics and a vehicle dynamics subject to stochastic disturbance.
△ Less
Submitted 8 July, 2023; v1 submitted 21 January, 2022;
originally announced January 2022.
-
A Compositional Approach to Parity Games
Authors:
Kazuki Watanabe,
Clovis Eberhart,
Kazuyuki Asada,
Ichiro Hasuo
Abstract:
In this paper, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We introduce the category of open parity games, which is defined using standard definitions for graph games. We also define a graphical language for open parity games as a prop, which have recently been used in many application…
▽ More
In this paper, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We introduce the category of open parity games, which is defined using standard definitions for graph games. We also define a graphical language for open parity games as a prop, which have recently been used in many applications as graphical languages. We introduce a suitable semantic category inspired by the work by Grellois and Melliès on the semantics of higher-order model checking. Computing the set of winning positions in open parity games yields a functor to the semantic category. Finally, by interpreting the graphical language in the semantic category, we show that this computation can be carried out compositionally.
△ Less
Submitted 28 December, 2021;
originally announced December 2021.
-
Architecture-Guided Test Resource Allocation Via Logic
Authors:
Clovis Eberhart,
Akihisa Yamada,
Stefan Klikovits,
Shin-ya Katsumata,
Tsutomu Kobayashi,
Ichiro Hasuo,
Fuyuki Ishikawa
Abstract:
We introduce a new logic named Quantitative Confidence Logic (QCL) that quantifies the level of confidence one has in the conclusion of a proof. By translating a fault tree representing a system's architecture to a proof, we show how to use QCL to give a solution to the test resource allocation problem that takes the given architecture into account. We implemented a tool called Astrahl and compare…
▽ More
We introduce a new logic named Quantitative Confidence Logic (QCL) that quantifies the level of confidence one has in the conclusion of a proof. By translating a fault tree representing a system's architecture to a proof, we show how to use QCL to give a solution to the test resource allocation problem that takes the given architecture into account. We implemented a tool called Astrahl and compared our results to other testing resource allocation strategies.
△ Less
Submitted 22 July, 2021;
originally announced July 2021.
-
Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications
Authors:
Sasinee Pruekprasert,
Clovis Eberhart,
Jérémy Dubut
Abstract:
We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller for two objectives: the first one is modelled as a right-recursive LTL formula, and the second one is to ensure that the average communication rate between the controller and the…
▽ More
We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller for two objectives: the first one is modelled as a right-recursive LTL formula, and the second one is to ensure that the average communication rate between the controller and the system stays below a given threshold. We translate the control problem to solving a mean-payoff parity game played on a discrete graph. Apart from extending the class of specifications, we propose a heuristic method to shorten the computation time. Finally, we illustrate our results on the example of a navigating nonholonomic robot with several specifications.
△ Less
Submitted 20 December, 2021; v1 submitted 30 March, 2021;
originally announced March 2021.
-
Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs
Authors:
Ichiro Hasuo,
Yuichiro Oyabu,
Clovis Eberhart,
Kohei Suenaga,
Kenta Cho,
Shin-ya Katsumata
Abstract:
We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation} -- in a nontrivial manner so that the two ideas boost the benefits of each other. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs…
▽ More
We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation} -- in a nontrivial manner so that the two ideas boost the benefits of each other. We implemented our algorithm on top of Anglican. The experimental results demonstrate our algorithm's efficiency, especially for programs with while loops and rare observations.
△ Less
Submitted 29 September, 2023; v1 submitted 5 January, 2021;
originally announced January 2021.
-
Symbolic Self-triggered Control of Continuous-time Non-deterministic Systems without Stability Assumptions for 2-LTL Specifications
Authors:
Sasinee Pruekprasert,
Clovis Eberhart,
Jérémy Dubut
Abstract:
We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issue…
▽ More
We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issued only when necessary, which saves energy. To this end, we first quantise the state and input spaces, and then translate the controller synthesis problem to the computation of a winning strategy in a mean-payoff parity game. We illustrate the feasibility of our method on the example of a navigating nonholonomic robot.
△ Less
Submitted 22 October, 2020;
originally announced October 2020.
-
Moment Propagation of Discrete-Time Stochastic Polynomial Systems using Truncated Carleman Linearization
Authors:
Sasinee Pruekprasert,
Toru Takisaka,
Clovis Eberhart,
Ahmet Cetinkaya,
Jérémy Dubut
Abstract:
We propose a method to compute an approximation of the moments of a discrete-time stochastic polynomial system. We use the Carleman linearization technique to transform this finite-dimensional polynomial system into an infinite-dimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finite-dimensional linear deterministic system, which we the…
▽ More
We propose a method to compute an approximation of the moments of a discrete-time stochastic polynomial system. We use the Carleman linearization technique to transform this finite-dimensional polynomial system into an infinite-dimensional linear one. After taking expectation and truncating the induced deterministic dynamics, we obtain a finite-dimensional linear deterministic system, which we then use to iteratively compute approximations of the moments of the original polynomial system at different time steps. We provide upper bounds on the approximation error for each moment and show that, for large enough truncation limits, the proposed method precisely computes moments for sufficiently small degrees and numbers of time steps. We use our proposed method for safety analysis to compute bounds on the probability of the system state being outside a given safety region. Finally, we illustrate our results on two concrete examples, a stochastic logistic map and a vehicle dynamics under stochastic disturbance.
△ Less
Submitted 24 February, 2021; v1 submitted 28 November, 2019;
originally announced November 2019.
-
Simple game semantics and Day convolution
Authors:
Clovis Eberhart,
Tom Hirschowitz,
Alexis Laouar
Abstract:
Game semantics has provided adequate models for a variety of programming languages, in which types are interpreted as two-player games and programs as strategies. Melliès (2018) suggested that such categories of games and strategies may be obtained as instances of a simple abstract construction on weak double categories. However, in the particular case of simple games, his construction slightly di…
▽ More
Game semantics has provided adequate models for a variety of programming languages, in which types are interpreted as two-player games and programs as strategies. Melliès (2018) suggested that such categories of games and strategies may be obtained as instances of a simple abstract construction on weak double categories. However, in the particular case of simple games, his construction slightly differs from the standard category. We refine the abstract construction using factorisation systems, and show that the new construction yields the standard category of simple games and strategies. Another perhaps surprising instance is Day's convolution monoidal structure on the category of presheaves over a strict monoidal category.
△ Less
Submitted 16 October, 2018;
originally announced October 2018.
-
What's in a game? A theory of game models
Authors:
Clovis Eberhart,
Tom Hirschowitz
Abstract:
Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We set out to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction,…
▽ More
Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies. We set out to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction, for any game setting, of a category of games and strategies. Furthermore, we extend the framework to deal with innocence, and prove that innocent strategies form a subcategory. We finally show that our constructions cover many concrete cases, mainly among the early models and the very recent sheaf-based ones.
△ Less
Submitted 29 November, 2017;
originally announced November 2017.
-
An intensionally fully-abstract sheaf model for $π$ (expanded version)
Authors:
Clovis Eberhart,
Tom Hirschowitz,
Thomas Seiller
Abstract:
Following previous work on CCS, we propose a compositional model for the $π$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it…
▽ More
Following previous work on CCS, we propose a compositional model for the $π$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $π$-calculus traces in the spirit of string diagrams.
△ Less
Submitted 14 November, 2017; v1 submitted 18 October, 2017;
originally announced October 2017.
-
Revisiting the quadrisection problem of Jacob Bernoulli
Authors:
Carl Eberhart
Abstract:
Two perpendicular segments which divide a given triangle into 4 regions of equal area is called a quadrisection of the triangle. Leonhard Euler proved in 1779 that every scalene triangle has a quadrisection with its triangular part on the middle leg. We provide a complete description of the quadrisections of a triangle. For example, there is only one isosceles triangle which has exactly two quadri…
▽ More
Two perpendicular segments which divide a given triangle into 4 regions of equal area is called a quadrisection of the triangle. Leonhard Euler proved in 1779 that every scalene triangle has a quadrisection with its triangular part on the middle leg. We provide a complete description of the quadrisections of a triangle. For example, there is only one isosceles triangle which has exactly two quadrisections.
△ Less
Submitted 21 November, 2016;
originally announced November 2016.
-
Fully-abstract concurrent games for pi
Authors:
Clovis Eberhart,
Tom Hirschowitz,
Thomas Seiller
Abstract:
We define a semantics for Milner's pi-calculus, with three main novelties. First, it provides a fully-abstract model for fair testing equivalence, whereas previous semantics covered variants of bisimilarity and the may and must testing equivalences. Second, it is based on reduction semantics, whereas previous semantics were based on labelled transition systems. Finally, it has a strong game semant…
▽ More
We define a semantics for Milner's pi-calculus, with three main novelties. First, it provides a fully-abstract model for fair testing equivalence, whereas previous semantics covered variants of bisimilarity and the may and must testing equivalences. Second, it is based on reduction semantics, whereas previous semantics were based on labelled transition systems. Finally, it has a strong game semantical flavor in the sense of Hyland-Ong and Nickau. Indeed, our model may both be viewed as an innocent presheaf semantics and as a concurrent game semantics.
△ Less
Submitted 16 October, 2013;
originally announced October 2013.
