An O(m log n) algorithm for branching bisimilarity on labelled transition systems
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 22 | |
| Author | ||
| Contributors | ||
| License | CC Attribution 3.0 Germany: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/55026 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
| |
| Keywords |
00:00
System programmingDynamic random-access memoryModemWorld Wide Web ConsortiumGoodness of fitSimilarity (geometry)State transition systemAlgorithm
00:15
AlgorithmSimulationEquivalence relationData structureSystem programmingMathematical analysisComplex (psychology)Database transactionState of matterTranslation (relic)CASE <Informatik>Multiplication signAuthorizationEquivalence relationSimulationAlgorithmLogicNeuroinformatikLecture/Conference
01:36
BisimulationSystem programmingAlgorithmGroup actionSimilarity (geometry)AlgorithmState transition systemLecture/Conference
01:48
Execution unitAlgorithmGroup actionNumberSimilarity (geometry)State of matterMultiplication signPartition of a setCalculationComplex (psychology)Equivalence relationHeegaard splittingSemiconductor memoryDigitizingTranslation (relic)Arrow of timeEndliche ModelltheorieSet (mathematics)Identical particlesAverageCombinational logicAlgorithmBookmark (World Wide Web)State transition systemMereologyOrder (biology)LogarithmMoment (mathematics)BitSquare numberTotal S.A.Invariant (mathematics)Revision controlSocial classLogical constantProcess (computing)QuotientTraffic reportingRun time (program lifecycle phase)Block (periodic table)TheoryGreatest elementSuite (music)Web pageMaxima and minimaOverhead (computing)Branch (computer science)Theory of relativityCASE <Informatik>Hydraulic jumpDifferent (Kate Ryan album)Proof theoryExterior algebraPrime idealSimulationVulnerability (computing)Data structureBenchmarkDiffuser (automotive)
Transcript: English(auto-generated)
00:01
Good morning, good afternoon, ladies and gentlemen. Welcome to this TACAS 2020 presentation. I'm going to show you the main ideas of our fast algorithm for branching by similarity on label transition systems. Perhaps you remember that five years ago, TACAS was held as a physical conference in the Netherlands.
00:23
At that conference, two authors presented a paper entitled an O of m log n algorithm for stuttering equivalence and branching by simulation. The two other authors then showed that in a few cases, it's not actually O of m log n.
00:41
I don't want to be too negative about the algorithm. It was quite fast already, we will see that also. Only it handled a few corner cases sub-optimally. The four of us together repaired the problem in the TACAS special issue of transactions of computational logic by putting a large and ugly bandage over the problem.
01:05
And actually, the algorithm handled branching by simulation by a translation to stuttering equivalence. This translation blows up the problem, and so the time complexity becomes a little bit bigger. Today, I'm presenting a solution to both.
01:22
We peeled off that bandage, and simplified the handling of new bottom states. Our current article also handles branching by simulation directly, so it is truly O of m log n. And that explains the title of our TACAS 2020 publication,
01:41
an O of m log n algorithm for branching by similarity on labeled transition systems. Now, what is a labeled transition system? Labeled transition systems are often explained using coffee machines. This is the model of a coffee machine that also can provide hot water,
02:00
the favorite drink of many Chinese. The gray arrows show internal transitions. For the user, the three states at the top and at the very bottom cannot be distinguished. So there is a non-trivial set of indistinguishable behaviors here. And when we minimize this LTS,
02:21
the three states become just one, and this is what remains. Now let's make this model a little bit more interesting. At some moment in time, the coffee may run out. This is also an internal action. The coffee machine decides on its own when there is not enough coffee powder left
02:42
to provide one more cup of coffee. Still, the two states on top can be distinguished by visible actions that happen afterwards. Therefore, we have two non-trivial sets of indistinguishable behaviors. And when we minimize this,
03:01
we find the internal transition still to be in the minimized LTS. Branching by similarity is the relation that describes these indistinguishable behaviors. First, let me show you what a branching by simulation is. If a relation describes these indistinguishable behaviors,
03:24
and two states, S and T, are related, and state S has a transition to S', then T should have a similar transition to T', and S' and T' are also indistinguishable. For T to T',
03:40
we allow that T first takes a few internal steps before it actually takes the visible transition with the same label as from S. But to avoid that the states that T visits in between jump too far off, we require that the last state Tn, just before it takes the visible transition,
04:01
is also related to the original state S. Branching by similarity now is the largest of these relations. It is the union of all branching by simulations, and it is the coarsest branching by simulation. What is the smallest model that is indistinguishable?
04:22
This question is answered by branching by similarity minimization. There are a number of algorithms to minimize a label transition system. For strong by similarity, that is by similarity without internal actions, there is the algorithm of Kanellakis and Smolka
04:41
that was quite quickly accelerated by Page and Tarjan to O of m log n. For branching by similarity, including these internal actions, Grothe and van Drager found an algorithm. Shortly after, Kanellakis and Smolka found one for strong by similarity.
05:00
But it took much longer to accelerate this. More than 25 years later, we, in our previous publication, accelerated this algorithm with the ugly bandage. I have to say that actually these O of m log n algorithms, both of Page Tarjan and our earlier algorithm,
05:22
had almost complexity O of m log n. And Valmarie found a trick to make the algorithm truly O of m log n on label transition systems in 2009. And we combine our earlier algorithm with the one of Valmarie here. Additionally, we simplified the handling of new bottom states.
05:45
All these algorithms that I've mentioned are based on partition refinement. The idea of partition refinement is to approximate an equivalence relation from above. You start with a coarse partition. For example, you assume that all states are equivalent.
06:00
You have a partition with only one equivalence class, or one block. Namely, all states are in one class. And then there may be some problems with this equivalence relation. So, you repair the problem by refining one of these blocks into multiple sub-blocks.
06:21
Once all the problems have been solved, you have reached the true equivalence relation. Now, to work efficiently, the faster algorithms remember the solved problems to avoid repeating work. They do that by a second partition. Page and Tarjan use a second partition
06:41
on the states to remember the solved problems. And Valmarie actually uses a partition of transitions. And that is what we are using here, too. So, we have these two partitions. A main partition of states into blocks. States in different blocks are shown to be not branching by similar.
07:02
So, the algorithm has found a proof that they are not branching by similar. And the auxiliary partition of transitions into bunches, transitions in different bunches cannot simulate each other. I will explain that shortly. And blocks have been split accordingly.
07:22
So, problems caused by these two transitions have been solved. What does it mean that transitions can simulate each other? Remember the definition of branching by simulation. We have there a transition from S to S prime and a transition from TN to T prime.
07:42
If two transitions can be in such a diagram, then they can simulate each other. If the transitions cannot be in such a diagram, then they cannot simulate each other. In our algorithm, we refine these two partitions alternatively.
08:01
So, we start with two coarse initial partitions. We first find a problem in the partition of transitions and replace it by a finer partition. That violates the invariant. So, there is now a problem also in the partition of states that we resolve and replace the partition of states with a finer partition.
08:22
Then there may be another problem in the partition of transitions that we solve. And again, a problem in the partition of states pops up and we solve that as well. And so we go on, alternatively refining the partition of transitions and the partition of states until we find that there is no more problem
08:41
in the partition of transitions. And then, by these invariants also, the partition of states has no problems anymore and it contains the true equivalence classes. To make it efficient, we use the principle, process the smaller half.
09:02
Because the actual refinement of these partitions is very similar to what we did in the previous publications, I only mention this principle. When we refine a block, we only process the states that are in the smaller resulting sub-block. And if we process a block of states,
09:20
then we also process their transitions. As a result, each transition is processed at most log n times. And that gives a total run time in the order of number of transitions times logarithm of number of states. The main new part of our algorithm
09:42
pertains to bottom states. What are bottom states? Look, in this block, the state on the left has a transition, an invisible transition, a grey arrow, to another state in the same block. That means it is a non-bottom state.
10:02
Bottom states, like the two states on the right, have no such transitions. Now I can ask, this bottom state down here has a yellow transition. Can the left non-bottom state simulate this transition? Well, itself, it doesn't have a yellow transition. But what it can do is
10:21
you can just take the grey arrow, the internal transition, and try again. Oh yes, that state has a yellow transition. What it means is we can ignore non-bottom states when we decide whether a block needs to be split or not.
10:40
Non-bottom states simulate other states trivially. But what may happen is that for some other reason, this block is split into two parts and that non-bottom state over there becomes a bottom state. Bottom states can cause problems, but we don't know whether this state
11:01
simulates or does not simulate other states. So we need to resolve these problems. What I want you to remember is only bottom states can cause problems in the partition of states. And when splitting a block, more states can become bottom states.
11:21
Now, to resolve these problems, we only need to register additional splitters to restore the invariant for these new bottom states. Splitters, that is a way to record problems that need to be solved right now. And to register these splitters,
11:41
we only require time that is proportional to the outgoing transitions of the new bottom states. So when we sum up over all states, we get a total time in the order of number of total transitions. Overall time complexity. Let's look at that.
12:01
I've already explained the time spent on new bottom states. Further running time is assigned to splitting the two partitions. So for the partition of states, a state is processed at most log n times. And every time when this happens, we spend time that is proportional
12:22
to the incoming and outgoing transitions of this state. Summing up over the states, we spend time, total number of transitions times log n. For the partition of transitions, a single transition is processed at most log of n square plus one times.
12:44
And whenever this happens, constant time is spent on that transition. Now log of n square is two times log n. So when we sum up over all the transitions, we spend time in order of number of transitions times log n.
13:03
Overall, everything fits within number of transitions times logarithm of number of states. And that is the worst case time complexity. The algorithm is efficient in theory. But sometimes the overhead
13:20
of an efficient algorithm is so large that it is slow in practice. To check for that, we ran the 31 largest benchmarks from the very large transition system suite and three of our own. We compared our algorithm with three older algorithms
13:41
all in the toolset MCRL2. So the traditional Grothe-Fandracher algorithm from 1990 has time complexity O of mn. It takes a long time, but it is quite memory efficient. Blohm and Orzan in 2003 have devised an algorithm
14:01
that has an even worse theoretical complexity, but in practice it is much faster. It comes at the cost of using additional memory. Our previous algorithm, which was almost O of m log n, is much faster than either of these, but again at yet more cost in memory.
14:24
I think the main problem of our previous algorithm is that it handles labeled transition systems by a translation to Kripke structures to stuttering equivalents, so it needs to store all the data twice. And today's algorithm, which is truly O of m log n,
14:41
is the fastest of all and also needs the same amount of memory as the Grothe-Fandracher algorithm, so it doesn't have any memory disadvantage. To get at these figures, we run every combination 10 times, and here we report the averages
15:00
rounded to significant digits. In conclusion, the algorithm that I presented is the fastest and most memory efficient algorithm for branching by similarity, both in theory and in practice. It is simpler than our previous algorithm
15:22
from ACM TOCL 2017. Now, branching by similarity is not only useful in itself, but it is also used for pre-processing if you want to calculate another behavioral equivalence, for example, weak by similarity. You can accelerate the calculation of that
15:40
by first calculating branching by similarity and then weak by similarity on the quotient. There is a technical report version of our publication that contains a few additional details, and it's all implemented in the tool MCRL2 from Eindhoven University, and you can download that from the website
16:02
www.mcrl2.org. I thank you for your attention, and I hope to see you in person soon again.