key: cord-0059619-c44ucj6z
authors: Bisping, Benjamin; Nestmann, Uwe
title: A Game for Linear-time–Branching-time Spectroscopy
date: 2021-03-01
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-72016-2_1
sha: ed141c9b6e79bf9caca75aa1135d322696a90c06
doc_id: 59619
cord_uid: c44ucj6z

We introduce a generalization of the bisimulation game that can be employed to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. By measuring the use of expressive powers, we adapt the formula generation to just yield formulas belonging to the coarsest distinguishing behavioral preorders/equivalences from the linear-time–branching-time spectrum. The induced algorithm can determine the best fit of (in)equivalences for a pair of processes.

Have you ever looked at two system models and wondered what would be the finest notions of behavioral equivalence to equate them-or, conversely: the coarsest ones to distinguish them? We run into this situation often when analyzing models and, especially, when devising examples for teaching. We then find ourselves fiddling around with whiteboards and various tools, each implementing different equivalence checkers. Would it not be nice to decide all equivalences at once? Example 1. Consider the following CCS process P 1 = a.(b + c) + a.d. It describes a machine that can be activated (a) and then either is in a state where one can choose from b and c or where it can only be deactivated again (d). P 1 shares a lot of properties with P 2 = a.(b + d) + a.(c + d). For example, they have the same traces (and the same completed traces). Thus, they are (completed) trace equivalent.

But they also have differences. For instance, P 1 has a run where it executes a and then cannot do d, while P 2 does not have such a run. Hence, they are not failure equivalent. Moreover, P 1 may perform a and then choose from b and c, and P 2 cannot. This renders the two processes also not simulation equivalent. Failure equivalence and simulation equivalence are incomparable-that is, neither one follows from the other one. Both are coarsest ways of telling the processes apart. Other inequivalences, like bisimulation inequivalence, are implied by both.

In the following, we present a uniform game-based way of finding the most fitting notions of (in)equivalence for process pairs like in Ex. 1.

Our approach is based on the fact that notions of process equivalence can be characterized by two-player games. The defender's winning region in the game corresponds to pairs of equivalent states, and the attacker's winning strategies correspond to distinguishing formulas of Hennessy-Milner logic (HML).

Each notion of equivalence in van Glabbeek's famous linear-time-branching-time spectrum [10] can be characterized by a subset of HML with specific distinguishing power. Some of the notions are incomparable. So, often a process pair that is equivalent with respect to one equivalence, is distinguished by a set of slightly coarser or incomparable equivalences, without any one of them alone being the coarsest way to distinguish the pair. As with the spectrum of light where a mix of wave lengths shows to us as a color, there is a "mix" of distinguishing capabilities involved in establishing whether a specific equivalence is finest. Our algorithm is meant to analyze what is in the mix.

Contributions. This paper makes the following contributions:

-We introduce a special bisimulation game that neatly characterizes the distinguishing formulas of HML for pairs of states in finite transition systems (Subsection 3.1 and 3.2). -We show how to enumerate the relevant distinguishing formulas using the attacker's winning region (Subsection 3.3). -We give a way of constructing a finite set of distinguishing formulas guaranteed to contain observations of the weakest possible observation languages, which can be seen as a "spectroscopy" of the differences between two processes (Subsection 3.4). -We present a small web tool that is able to run the algorithm on finite-state processes and output a visual representation of the game (Section 4). We also report on the distinctions it finds for all the finitary examples from the report version of the linear-time-branching-time spectrum [12] .

We frame the contributions by a roundtrip through the basics of HML, games and the spectrum (Section 2), a discussion of related work (Section 5), and concluding remarks on future lines of research (Section 6).

We use the concepts of transition systems, games, observations, and notions of equivalence, largely due to the wake of Hennessy and Milner's seminal paper [14] .

Labeled transition systems capture a discrete world view, where there is a current state and a branching structure of possible state changes to future states.

Definition 1 (Labeled transition system). A labeled transition system is a tuple S = (P, Σ, →) where P is the set of states, Σ is the set of actions, and → ⊆ P × Σ × P is the transition relation.

Hennessy-Milner logic [14] describes finite observations (or "tests") that one can perform on such a system. We often just write {ϕ 0 , ϕ 1 , ...} for i∈I ϕ i . T denotes ∅, the nil-element of the syntax tree, and a is a short-hand for a T. Let us also implicitly assume that formulas are flattened in the sense that conjunctions do not contain other conjunctions as immediate subformulas. We will sometimes talk about the syntax tree height of a formula and consider the height of T to equal 0.

Intuitively, a ϕ means that one can observe a system transition labeled by a and then continue to make observation(s) ϕ. Conjunction and negation work as known from propositional logic. We will provide a common game semantics for HML in the following subsection.

Let us fix some notions for Gale-Stewart-style reachability games where the defender wins all infinite plays. Definition 4 (Plays and wins). We call the paths

The defender wins infinite plays. If a finite play g 0 . . . g n is stuck, the stuck player loses: The defender wins if g n ∈ G a , and the attacker wins if g n ∈ G d . All Gale-Stewart-style reachability games are determined, that is, W a ∪ W d = G. The winning regions of finite simple reachability games can be computed in linear time of the number of game moves (cf. [13] ). This is why the spectroscopy game of this paper can easily be used in algorithms. It derives from the following game.

Definition 7 (HML game). For a transition system S = (P, Σ, →), the HML game G S

, where the defender controls observations and negated conjunctions, that is (p, a ϕ) ∈ G d and (p, ¬ i∈I ϕ i ) ∈ G d (for all ϕ, p, I), and the attacker controls the rest. There are five kinds of moves:

Like in other logical games in the Ehrenfeucht-Fraïssé tradition, the attacker plays the conjunctions and universal quantifiers, whereas the defender plays the disjunctions and existential quantifiers. For instance, (p, a ϕ) is declared as defender position, since a ϕ is meant to become true precisely if there exists a state p reachable p a → p where ϕ is true. As every move strictly reduces the height of the formula, the game must be finite-depth (and cycle-free), and, for image-finite systems and formulas, also finite. It is determined and the following semantics is total. is false: No matter whether the defender plays to (b + d, ¬ d T) or to (c + d, ¬ d T), the attacker wins by moving to the stuck defender position (0, ¬T). (Recall that T is the empty conjunction and that 0 is the completed process!)

Definition 9 (Distinguishing formula). A formula ϕ distinguishes state p from q iff ϕ p is true and ϕ q is not. 1

, preorders two states p, q, written p X q, iff no formula ϕ ∈ O X distinguishes p from q. If p X q and q X p, then the two are X-equivalent, written p ≡ X q.

Definition 11 (Linear-time-branching-time languages [12] ). The lineartime-branching-time spectrum is a lattice of observation languages (and of entailed process preorders and equivalences). Every observation language O X can perform trace observations, that is, T ∈ O X and, if ϕ ∈ O X , then a ϕ ∈ O X . At the more linear-time side of the spectrum we have:

At the more branching-time side, we have simulation observations. Every simula-

The observation languages of the spectrum differ in how many of the syntactic features of HML one will encounter when descending into a formula's syntax tree. We will come back to this in Subsection 3.4.

Note that we consider {ϕ} to be an alias for ϕ. With this aliasing, all the listed observation languages are closed in the sense that all subformulas of an observation are themselves part of that language. They thus are inductive in the sense that all observations must be built from observations of the same language with lower syntax tree height.

This section introduces our main contribution: the spectroscopy game (Def. 13), and how to build all interesting distinguishing HML formulas from its winning region (Def. 14). To justify our construction and to prove that we indeed find distinguishing formulas (Thm. 1), let us first examine the formula preorder game (Def. 12), which is closer to the problem whether formulas are (non-)distinguishing.

Def. 10 entails a straightforward way of turning the problem whether a set of observations O ⊆ O X preorders two states p, q into a game: Have the attacker pick a supposedly distinguishing formula ϕ ∈ O, and then have the defender choose whether to play the HML game (Def. 7) for ¬ϕ p or for ϕ q . This direct route will yield infinite games for infinite O-and all the languages from Def. 11 are infinite! To bypass the infinity issue, we will introduce a variation of this game where the attacker gradually chooses their attacking formula. In particular, this means that the attacker now decides which observations to play. In return, the defender does not need to pick a side in the beginning and may postpone the decision where (on the right-hand side) an observation leads. Postponing decisions here means that the defender may play non-deterministically, moving to multiple states at once. The mechanics are analogous to the standard powerset construction when transforming non-deterministic finite automata into deterministic ones. 

The formula preorder game precisely characterizes whether an observation language is distinguishing:

Proof (Sketch). By induction over the height of formulas in O X with arbitrary p and Q, and strengthening the induction predicate to not only consider ϕ but also partial conjunctions O with O ⊆ O whenever ϕ = O . To prove the right-to-left direction, exploiting the determinacy of the game is convenient. 

Let us now remove the formulas from the formula game (Def. 12). The idea is to look at the game for the whole of HML, called G B . Only attack moves in the formula game change the current set of observations, and they are completely guided by the context-free grammar of HML (Def. 2). Therefore, we can 3 assume O to equal HML[Σ] in every reachable position of G B . Effectively, O can be canceled out of the game, without losing any information. We call the remaining game the "spectroscopy game." Figure 1 gives a graphical representation. 

We have already introduced two tricks in this definition to ease formula reconstruction in the next subsection. (1) The attack moves are labeled with the syntactic constructs from which they originate. This does not change expressive power.

(2) Negation moves are restricted to situations where Q = {q}. After all, winning attacker strategies will pay attention to only playing a negation after minimizing the odds of being put on a bad position, anyways. Note that, like in the formula game with arbitrary-depth formulas, the attacker could force infinite plays by cycling through conjunction moves (and also negation moves). However, they will not do this, as infinite plays are won by the defender. This fact is a corollary of the well-known Hennessy-Milner theorem (HML characterizes bisimilarity), given that G is constructed as a simplification of G B .

Comparing G to the standard bisimulation game from the literature (with symmetry moves, see e.g. [3] ), we can easily transfer attacker strategies from there. In the standard game, the attacker will play (p, q) (a, p , q) with p a → p and the defender has to answer by (a, p , q) (p , q ) with q a → q . In the spectroscopy game, the attacker can enforce analogous moves by playing

The opposite direction of transfer is not so easy, as the attacker has more ways of winning in G . But this asymmetry is precisely why we have to use the spectroscopy game instead of the standard bisimulation game if we want to learn about, for example, interesting failure-trace attacks.

Due to the subset construction over P, the game size clearly is exponential in the size of the state space. Going exponential is necessary, as we want to also characterize weaker preorders like the trace preorder, where exponential P-subset or Σ * -word constructions cannot be circumvented. However, for moderate realworld systems, such constructions will not necessarily show their full exponential blow-up (cf. [6] ).

For concrete implementations, the subset construction also means that the costs of storing game nodes and of comparing two nodes is linear in the state space size. Complexity-wise this factor is dominated by the overall exponentialities.

Definition 14 (Strategy formulas). Given an attacker strategy F ⊆ (G a × L × G) for the spectroscopy game G , the set of strategy formulas, Strat F (g a ), is inductively defined by:

if ϕ ∈ Strat F (g a ) and (g a , ¬, g a ) ∈ F , then ¬ϕ ∈ Strat F (g a ), and if ϕ g a ∈ Strat F (g a ) for all g a ∈ I = {g a | g d * g a }, and (g a , ∧, g d ) ∈ F , then g a ∈I ϕ g a ∈ Strat F (g a ). Definition 15 (Winning strategy graph). Given the attacker winning region W a and a starting position g 0 ∈ W a , the attacker winning strategy graph F a is the subset of the -graph that can be visited from g 0 when following all -edges unless they lead out of W a . This graph can be cyclic. However, if the attacker plays inside their winning region according to F a , they will always have paths to their final winning positions. So even though the attacker could loop (and thus lose), they can always end the game and win in the sense of Def. 5. Note that the theorem is only one-way, as every distinguishing formula can neutrally be extended by saying that some additional clause that is true for both processes does hold. Def. 14 will not find such bloated formulas. Due to cycles in the game graph, Strat Fa will usually yield infinitely many formulas. But we can become finite by injecting some way of discarding long formulas that unfold negation cycles or recursions of the underlying transition system. The next section will discuss how to do this without discarding the formulas that are interesting from the point of view of the spectrum.

In our quest for the coarsest behavioral preorders (or equivalences) distinguishing two states, we actually are only interested in the ones that are part of the smallest observation languages from the spectrum (Def. 11). We can think of the amount of HML-expressiveness used by a formula as its price.

Let us look at the price structure of the spectrum from Def. 11. Table 1 gives an overview of how many syntactic HML-features the observation languages may use at most. (If formulas use fewer, they still are considered part of that observation language.) So, we are talking budgets, in the price analogy. We say that a formula ϕ 1 dominates ϕ 2 if ϕ 1 has lower or equal values than ϕ 2 in each dimension of the metrics with at least one entry strictly lower. Let us note the following facts: 1. When formulas are constructed recursively, like the strategy formulas in Def. 14, they can only contribute to dominating (i.e. more expensive) or equivalently valued formulas with respect to the metrics. 2. Formulas can be incomparable. For example, a { b , c } and a ¬ a , corresponding to coordinates (1,0,2,0,0) and (1,0,0,1,1), are incomparable. 3. A locally more expensive formula may pay off as part of a bigger global formula. For example, if two states are distinguished by ¬ a and b , the dominated formula ¬ a may later be handy to construct a (comparably cheap) failure formula.

These observations justify our algorithm to prune all formulas from the set Strat Fa (g) that are dominated with respect to the metrics by any other formula in this set, unless they are impossible trace futures of the form ¬ a 1 a 2 .... We moreover add formula height in terms of observations as a dimension in the metric, which leads to loop unfoldings being dominated by the shorter paths. Algorithm 1 shows all the elements in concert. It constructs the spectroscopy game G S (Def. 13) and computes its attacker winning strategy graph F a (Def. 15). If the attacker cannot win, the algorithm returns a bisimulation relation. Otherwise, it constructs the distinguishing formulas: It keeps a map strats of strategy formulas that have been found so far and a list of game positions todo that have to be updated. In every round, we take a game position g from todo. If some of its successors have not been visited yet, we add them to the top of the work list. Otherwise we call Strat Fa,strats (g) to compute distinguishing formulas using the follow-up formulas found so far strats. This function mostly corresponds to Def. 14 with the twist, that partial follow-ups are used instead of recursion, and that the construction for conjunctions is split onto attacker and defender positions. Of the found formulas, we keep only the non-dominated ones and impossible future traces. If the result changes strats(g), we enqueue each game predecessor to propagate the update there.

The algorithm structure is mostly usual fixed point machinery. It terminates because, for each state in a finite transition system, there must be a bound on the distinguishing mechanisms necessary with respect to our metrics, and Strat will only generate finitely many formulas under this bound. Keeping the impossible future formulas unbounded is alright, because they have to be constructed from trace formulas, which are subject to the bound.

We have implemented the game and the generation of minimal distinguishing formulas in the "Linear-time-Branching-time Spectroscope", a Scala.js program that can be run in the browser on https://concurrency-theory.org/ltbt-spectroscope/.

The tool (screenshot in Fig. 2) consists of a text editor to input basic CCS-style processes and a view of the transition system graph. When queried to compare two processes, the tool yields the cheapest distinguishing HML-formulas it can find for both directions. Moreover, it displays the attacker-winning part of the spectroscopy game overlayed over the transition system. The latter can also enlighten matters, at least for small and comparably deterministic transition systems. From the found formulas, the tool can also infer the finest fitting preorders for pairs of processes (Fig. 3) .

To "benchmark" the quality of the distinguishing formulas, we have run the algorithm on all the finitary counterexample processes from the report version of "The Linear-time-Branching-time Spectrum" [12] . Table 2 reports the output of our tool, on how to distinguish certain processes. The results match the (in)equivalences given in [12] . In some cases, the tool finds slightly better ways of distinction using impossible futures equivalence, which was not known at the time of the original paper. All the computed formulas are quite elegant / minimal.

For each of the examples (from papers) we have considered, the browser's capacities sufficed to run the algorithm in 30 to 250 milliseconds. This does not mean that one should expect the algorithm to work for systems with thousands of states. There, the exponentialities of game and formula construction would hit. However, such big instances would usually stem from preexisting models where one would very much hope for the designers to already know under which semantics to interpret their model. The practical applications of our browser tool are more on the research side: When devising compiler optimizations, encodings, or distributed algorithms, it can be very handy to fully grasp the equivalence structure of isolated instances. The Linear-time-Branching-time Spectroscope supports this process. Table 2 . Formulas found by our implementation for some interesting processes from [12] . 

The game and the algorithm presented fill a blank spot in between the following previous directions of work:

Distinguishing formulas in general. Cleaveland [5] showed how to restore (non-minimal) distinguishing formulas for bisimulation equivalence from the execution of a bisimilarity checker based on the splitting of blocks. There, it has been named as possible future work to extend the construction to other notions of the spectrum. We are not aware of any place where this has previously been done completely. But there are related islands like the encoding between CTL and failure traces by Bruda and Zhang [7] . There is also more recent work like Jasper et. al [15] extending to the generation of characteristic invariant formulas for bisimulation classes. Previous algorithms for bisimulation in-equivalence tend to generate formulas that alternate a and [b] observations while pushing negation to the innermost level. Such formulas can not as easily be linked to the spectrum as ours.

Game-characterizations of the spectrum. After Shukla et al. [18] had shown how to characterize many notions of equivalence by HORNSAT games, Chen and Deng [4] presented a hierarchy of games characterizing all the equivalences of the linear-time-branching-time spectrum. The games from [4] cannot be applied as easily as ours in algorithms because they allow word moves and thus are infinite already for finite transition systems with cycles. Constructing distinguishing formulas from attacker strategies of these games would be less convenient than in our solution. Their parametric approach is comparable to fixing maximal price budgets ex ante. Our on-the-fly picking of minimal prices is more flexible.

Using game-characterizations for distinguishing formulas. There is recent work by Mika-Michalski et al. [16] on constructing distinguishing formulas using games in a more abstract coalgebraic setting focussed on the absence of bisimulation. The game and formula generation there, however, cannot easily be adapted for our purpose of performing a spectroscopy also for weaker notions.

Alternatives. One can also find the finest notion of equivalence between two states by gradually minimizing the transition system with ever coarser equivalences from bisimulation to trace equivalence until the states are conflated (possibly also trying branches). Within a big tool suite of highly optimized algorithms this should be quite efficient. We preferred the game approach, because it can uniformly be extended to the whole spectrum and also has the big upside of explaining the in-equivalences by distinguishing formulas. An avenue of optimization for our approach, we have already tried, is to run the formula search on a directed acyclic subgraph of the winning strategy graph. For our purpose of finding most fitting equivalences, DAG-ification may preclude the algorithm from finding the right formulas. On the other hand, if one is mainly interested in a short distinguishing formula for instance, one can speed up the process with DAG-ification by the order of remaining game rounds.

In this paper, we have established a convenient way of finding distinguishing formulas that use a minimal amount of expressiveness.

System analysis tools can employ the algorithm to tell their users in more detail how equivalent two process models are. While the generic approach is costly, instantiations to more specific, symbolic, compositional, on-the-fly or depth-bounded settings may enable wider applications. There are also some algorithmic tricks (like building the concrete formulas only after having found the price bounds and heuristics in handling the game graph) we have not explored in this paper.

So far, we have only looked at strong notions of equivalence [10] . We plan to verify the game in Isabelle/HOL and to extend our algorithm, so it also deals with weak notions of equivalence [11] . These equivalences abstract over τ -actions representing "internal activity" and correspond to observation languages with a special temporal -observation (cf. [9] ). This would generalize work on weak game characterizations such as de Frutos-Escrig et al.'s [8] and our own [2, 3] . The vision is to arrive at one certifying algorithm that can yield finest equivalences and cheapest distinguishing formulas as witnesses for the whole discrete spectrum.

On a different note, our group is also working on an educational computer game about process equivalences. 5 The (theoretical) game of this paper can likely be adapted to go in the other direction: from formulas to distinguished transition systems. It may thereby synthesize levels for the (computer) game. So, in the end, all this might actually contribute to actual people having actual fun.

Linear-time-branching-time spectroscope: TACAS 2021 edition

Computing coupled similarity

Coupled similarity: the first 32 years

Game characterizations of process equivalences

On automatically explaining bisimulation inequivalence

Testing equivalence as a bisimulation equivalence

Model checking is refinement -from computation tree logic to failure trace testing

Games for bisimulations and abstraction

Congruence from the operator's point of view: Syntactic requirements on modal characterizations

The linear time-branching time spectrum

The linear time-branching time spectrum II. In: International Conference on Concurrency Theory

The linear time-branching time spectrum I -the semantics of concrete, sequential processes

Finite model theory and descriptive complexity

On observing nondeterminism and concurrency

Characteristic invariants in Hennessy-Milner logic

Explaining non-bisimilarity in a coalgebraic approach: Games and distinguishing formulas

A logical viewpoint on process-algebraic quotients

HORNSAT, model checking, verification and games

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Acknowledgments. We are thankful to members of our research group (especially Kim Völlinger), participants of our course Modelle Dynamischer Systeme, and the anonymous reviewers for lots of helpful comments.Data availability. The source code git repository of our implementation can be accessed via https://concurrency-theory.org/ltbt-spectroscope/code/. Code to reproduce the results presented in this paper is available on Zenodo [1] .