Hybrid games are a highly expressive way to model the interaction between cyber-physical systems. This high expressivity comes at the price of decidability. This work proposes an extension to hybrid games that adds the conditions prompting agents to move. We call this extension hybrid games with triggers (HGT). We show how this extension makes it possible to translate a hybrid game into a discrete game with countable state space. Modelling the interaction between multiple cyber-physical systems (CPS) is a critical problem in computer science, particularly in formal methods. Many approaches were presented to model and reason about this interaction, such as dynamic diferential logic [ 1], and its extension to diferential game logic [2], algebraic [3] and coalgebraic [4] approaches among many others.
(1) (2) Unlike time, a small set of formulas like 1 could be suficient to model a complete system. (3) As we show in this paper, given a countable language of real arithmetic [11], triggers reduce the hybrid game into a discrete game with countable state space. https://mase.kastel.kit.edu/team_qais_hamarneh.php (Q. Hamarneh)
CEUR
ceur-ws.org
In the next Section 1.1, we briefly overview the related work. Section 2 defines the hybrid games this work is based on. The main contribution of this work is presented in sections 3 and 4. In Section 3, we introduce the syntax and semantics of hybrid games with triggers, and we informally define the algorithm to create a discrete game based on an HGT in Section 4. We conclude in Section 5 with a summary and a look at future work.
This work can be seen as a hybrid extension of de Alfaro et al.’s timed games [
As already discussed, other ways to discretize hybrid games exist [
Tight durational concurrent game structures (TDCGS) [13] are intuitively similar to hybrid game with triggers. Transitions in TDCGS carry an integer time delay. This time, however, is treated as a cost and does not reflect the evolution of the continuous dynamics.
This definition of a hybrid game is adopted from [
Given a valuation ∈
is the set of all real arithmetic quantifier-free formulas over . ( ) and an arithmetic term , we write [ / ] for the valuation where all variables have the same value as in , except [ / ]( ) = ( ). This definition is extended to ordered sets of assignments, where the assignments are executed in order. Given a set of diferential equations has passed. A hybrid game G is a tuple: , we write [ , ] for the valuation updated according to the equations in after some time ∈ R≥0 0 ∈ a finite nonempty set of real-valued variables with typical elements 0, 1. a continuous transition relation that assigns each location ∈ a set of diferential equations associate each location with an invariant. { 1, 2, … , } a finite nonempty set of agents.
( ) = { ̇ = ∣ ∈ }. 1 ⊍ 2 ⊍ … ⊍
a disjoint union of finite nonempty sets of agents’ actions.
The typical actions of agent ∈
are , . a finite nonempty set of edges representing discrete transition relation with typical elements (, , , ,
′) such that: ● , ′ ∈ , ● ∈ ● ∈ ●
called a guard, an action for some ∈
, and is a finite (possibly empty) ordered set of assignments called a jump.
( ), ( ), ( ), ( ) and ( ) to reference the components of
A valuation enables the edge = (, , , ,
′) ∈ (we say the action ( ) is enabled) if: ● ⊧ ( ), ● ⊧ , and ● [ ] ⊧ ( ′) ∈ ⟨, ⟩ Ð
→ ⟨, ⟩ Ð→ ⟨
In a hybrid game, a configuration is a pair ⟨, ⟩ representing the game’s location ∈ and valuation ( ). ⟨ 0, 0⟩ is the initial configuration. Two types of transitions are possible: A time transition ⟨, ( ), ]⟩ for ∈ ≥0 is legal if for all ′ ∈ [0, ], [ ( ), ′] ⊧ ( ). An edge transition agent that takes the action
( ) ∈ ( )]⟩ for an edge ∈ with ( ) =
is a legal transition if enables . The
is called to blame for the edge transition. The other agents are
called blameless. A play is an infinite sequence of configurations
starts at the initial configuration and for each ∈ N0, there exists a legal transition ⟨ , ⟩ → ⟨ +1, +1⟩.
(⟨ 0, 0⟩, ⟨ 1, 1⟩, ⟨ 2, 2⟩, … ) which
Remark 1. In this paper, we assume all diferential equations to be solvable. Even with solvable diferential
equations, the question of whether there exists a play that reaches a certain configuration is undecidable in
a hybrid game [
In this section, we introduce an extension to the definition of hybrid games. We call this extension hybrid games with triggers or (HGT) for short. A trigger is an agent-declared quantifier-free formula of real arithmetic that, once satisfied, prompts the agent to take an action. Intuitively, the trigger is the reason the agent moves. An autonomous vehicle could set a trigger to be not enough free space ahead or the desired intersection is reached. According to the case that comes first, the car would have to take an action. An edge transition only happens when some agent has a satisfied trigger. With each edge transition, each agent gets to update their triggers. We call the set of all possible triggers for every location , (, , ⊥, ∅, configuration is ⟨ 0, 0, trig0⟩.
0, , 0, , , , ⊥, ⊥,
, trig0) is the initial triggers function. The set ⊥ includes a stutter , available for every agent. If an agent’s trigger is satisfied and this agent has no enabled , the agent must take the stutter action ⊥. This indicates that there is a self-loop edge ) ∈ ⊥. A configuration in a HGT is a triplet ⟨, , trig⟩. The initial if and only if its solution set is a closed set under the usual topology in R∣ ∣.
Trigger Formula:
A formula is called a trigger formula if and only if for every valuation and every map
assigning a diferential equation to each variable in , there exists a minimum time satisfied, i.e. [ , ∈ R≥0 to satisfy , i.e. such that [ , ] ⊭ for all ∈ R≥0. In other words, a formula is a trigger formula ( ∈ ) ] ⊧ and for all 0 ≤ ′ < , [ , ′ ] ⊭ , or if is never This restriction eliminates formulas like > 2 for a variable ∈ where no exact time exists when it is first satisfied if the valuation formula.
Given a valuation , a flow is extended to configurations formulas if such a time exists: ( ) = 0 and
( ) = 1. On the contrary, ≥ 2 is a valid trigger and a trigger , we define the function time to trigger or (, , ) ⟨, , trig⟩ to return the minimum time required to satisfy any of the to return the minimum time required to satisfy the trigger if it exists and ∞ otherwise. This definition (⟨, , trig⟩) = min { ( , , trig( )) ∣ ∈ } .
The definition of legal transitions in HGT is more restrictive than that in hybrid games. A transition is ⟨, , trig⟩ → ⟨ ′, ′, trig′⟩ legal if and only if it fulfils the following conditions: • ⟨, ⟩ → ⟨ ′, ′⟩ is legal in the hybrid game, • a time transition ⟨, , trig⟩ Ð→ ⟨, and ≤ (⟨, , trig⟩), and blame for the transition. • an edge transition ⟨, , trig⟩ Ð→ ⟨
( ), trig], trig⟩ does not change the triggers function trig, ( ), [ ( )], trig′⟩ if ⊧ ( ) for the agent ∈ to Along with each edge transition, each player gets to choose a new trigger ∈ time, the agent who gets to take an action is chosen at random.
( ) = . Similar to [
In this example, we can notice that robots (agents) do not need to calculate the time needed for the trigger to be satisfied when selecting one. Another observation is that a small set of trigger formulas is often suficient for many systems. This feature makes reasoning about the system significantly easier. (ℎ2, 3).
Remark 2. Contrary to guards and invariants, triggers are not part of the game structure but rather part of the players’ strategies. A player could choose diferent triggers in the same location (see Example 3.0.1). While it is possible to extend the game structure by adding more locations and more restrictive guards and invariants to embed the triggers into the game structure, this is not always possible with a finite set of locations.
Winning Conditions:
We adopt the winning conditions from [
) for the time convergence, i.e. the agent only takes a finite number of actions during the entire play. The set of winning plays for agent with the desired outcome is ( ( ) ∩ ) ∪ ( ⧵ ), where
( ) is the set of plays that fulfils . As noted in [
In this section, we show an intuitive way to define a discrete game, such that agent ∈ has a winning strategy in the HGT if and only if the same has a winning strategy in the discrete game. The intuition of the discrete game is to skip any time steps where no triggers are satisfied. This allows time to move in discrete steps. At any configuration ⟨, , trig⟩ with ⊭ trig( ) for all ∈ , the game can progress by (⟨, , trig⟩). If a trigger is satisfied, any enabled edge can be taken and the trigger function gets updated.
Due to space limitations, we only briefly describe the discrete game in this paper.
The discrete game is structured as a concurrent game structure (CGS) [14]. The players are the agents of the HGT with the addition of the player ∉ to select the agent who gets to take an action when more than one trigger is satisfied. While only one action is taken in each step, the game is concurrent to allow all agents to select new triggers simultaneously. The actions available for the agents are × . The actions available for are the set .
The set of states of the discrete game is defined inductively: • 0 = ⟨ 0, 0, trig0⟩ ∈ is the initial state. • If the state = ⟨, , trig⟩ ∈ , then: – if no trigger is satisfied ⊭ trig( ) for all ∈
⟨, [ ( ), (⟨, , trig⟩)], trig⟩ ∈ , – otherwise for every ∈ ⊥ enabled at and for every function trig′ ∶ → state ⟨ ( ), [ ( )], trig′⟩ ∈ . and (⟨, , trig⟩) ∈ R≥0, then , the A time-abstract game is visualized in Figure 2, where the game evolves only based on the players’ choices.
Given that the number of edges ⊥ is finite and the number of trigger formulas is countable [ 11], each
layer of the tree is countable. The state space of the entire discrete game is, therefore, countable. Each
discrete game state is labelled with formulas that its valuation satisfies and are relevant to the agents’
winning conditions. These formulas serve as atomic propositions in the discrete game. Additionally, the
states are labelled according to their position in the tree. We use a set of atomic propositions inspired
by [
A play is winning for an agent if (1) the play satisfies the desired outcome (expressed as a temporal property) and has an infinite number of states marked with or (2) the play has a finite number of states marked with and a finite number of states marked with . The existence of a winning strategy for the agent can be then expressed in the notation of ATL* [14] as follows: ⟪{ }⟫( ∧ ◻ ◇ ) ∨ (◇ ◻ ¬ ∧ ◇ ◻ ¬ ) (2) This reduces the winning conditions in a hybrid game with triggers to an ATL* model checking problem over countable state space. This is shown to be decidable in [15, 16].
Extending hybrid games with triggers has multiple advantages and applications beyond the decidable fragment of hybrid games brought on by triggers.
In addition to the significant decidability results, triggers could help improve system understandability. An AI system, for instance, could be trained to choose (or form) a trigger formula and not act again until this formula is satisfied. Such a feature would have major benefits to AI verification and explainability.
In summary, hybrid games with triggers (HGT) ofer a powerful framework for reasoning about and verifying multi-agent hybrid systems. We show that by incorporating agents’ rationale into the game model, HGT can efectively reduce a hybrid game to a decidable discrete game without restricting its continuous or discrete dynamics.
This research was supported by the Innovation Campus for Future Mobility (www.icm-bw.de) and by the German Research Foundation (DFG) within the Collaborative Research Center (CRC) 1608 Convide (www.sfb1608.kit.edu/index.php). Computer Science, Springer, 2003, pp. 142–156. URL: https://doi.org/10.1007/978-3-540-45187-7_9. doi:10.1007/978- 3- 540- 45187- 7\_9. [11] A. Tarski, A decision method for elementary algebra and geometry, in: B. F. Caviness, J. R. Johnson (Eds.), Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer Vienna, Vienna, 1998, pp. 24–84. [12] T. A. Henzinger, Hybrid automata with finite bisimulations, in: Z. Fülöp, F. Gécseg (Eds.), Automata,
Languages and Programming, Springer Berlin Heidelberg, Berlin, Heidelberg, 1995, pp. 324–335. [13] F. Laroussinie, N. Markey, G. Oreiby, Model-checking timed atl for durational concurrent game structures, in: International Conference on Formal Modeling and Analysis of Timed Systems, Springer, 2006, pp. 245–259. [14] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, J. ACM 49 (2002) 672–713.
URL: https://doi.org/10.1145/585265.585270. doi:10.1145/585265.585270. [15] S. Schewe, Atl* satisfiability is 2exptime-complete, in: International colloquium on automata, languages, and programming, Springer, 2008, pp. 373–385. [16] F. Mogavero, A. Murano, G. Perelli, M. Y. Vardi, Reasoning about strategies: On the model-checking problem, ACM Transactions on Computational Logic (TOCL) 15 (2014) 1–47.