CAAL 2.0: Recursive HML, Distinguishing Formulae, Equivalence Collapses and Parallel Fixed-Point Computations

Enevoldsen, Søren ; Olesen, Simon Reedtz ; Wortmann, Jacob Karstensen

4. term

Software, Master

2015

2015-06-09

108

Denne rapport beskriver nye funktioner i CAAL, en webbaseret undervisningsplatform til reaktive systemer (systemer der reagerer på input over tid). CAAL lader brugere beskrive processer i procesalgebraen Calculus of Communicating Systems (CCS), kontrollere forskellige præordener og ækvivalenser mellem processer, spille bisimulationsspil mod værktøjet for at forstå resultaterne og udføre modeltjek af rekursive Hennessy-Milner-formler (HML). Beregningerne udføres ved at omsætte problemer til afhængighedsgrafer og beregne fikspunkter løbende med en on-the-fly algoritme. I arbejdet her udvider vi CAAL med fuld syntaks og semantik for HML og giver reduktioner fra HML-formler til afhængighedsgrafer. For at supplere bisimulationsspillene introducerer vi et HML-spil og viser, at en formels opfyldelighed hænger sammen med, hvilken spiller der har en universel vindende strategi, altså en strategi der vinder uanset modstanderens træk. Vi viser også, at sådanne strategier svarer til fikspunkt-tildelinger på afhængighedsgraferne, hvilket forbinder opfyldelighed med disse tildelinger. Som alternativ til at spille bisimulationsspil viser vi, at man kan beregne en skelnende formel for to processer, der ikke er bisimilære. Det er svært at finde den enkleste formel; vi formoder, at det er NP-svært at afgøre, om en simpel formel findes. I stedet præsenterer vi en grådig algoritme, der kan forenkle nogle formler. CAAL kan vise processer visuelt, men graferne kan blive komplekse. Vi præsenterer teori og en algoritme, der forenkler ved at sammenlægge ækvivalente tilstande i ækvivalensklasser, så brugeren lettere kan fokusere på bestemte aspekter af en proces. Som et eksperiment forsøgte vi at genbruge CAAL-kode i en parallel algoritme. Vi dokumenterer design, pseudokode og test. Resultaterne var utilfredsstillende, og vi peger på mulige årsager.

This report describes new features added to CAAL, a web-based teaching tool for reactive systems (systems that respond to inputs over time). CAAL lets users describe processes in the process algebra Calculus of Communicating Systems (CCS), check various behavioral preorders and equivalences between processes, play bisimulation games against the tool to understand results, and model check recursive Hennessy-Milner logic (HML) formulas. It solves problems by reducing them to dependency graphs and computing fixed points on the fly with an on-the-fly algorithm. In this work, we extend CAAL with full HML syntax and semantics and provide reductions from HML formulas to dependency graphs. To complement bisimulation games, we introduce an HML game and show that whether a formula is satisfiable aligns with which player has a universal winning strategy, that is, a strategy that wins regardless of the opponent’s moves. We also show that such strategies correspond to fixed-point assignments on dependency graphs, linking satisfiability to those assignments. As an alternative to playing bisimulation games, we show it is possible to compute a distinguishing formula for two processes that are not bisimilar. Finding the simplest such formula is difficult; we conjecture that deciding whether a simple formula exists is NP-hard. Instead, we present a greedy algorithm that simplifies some formulas. CAAL can display visual process graphs, which can become complex. We present the theory and an algorithm for equivalence collapse: merging equivalent states into equivalence classes to simplify the graph and help users focus on relevant behavior. As an experiment, we attempted to reuse CAAL code in a parallel algorithm. We document the design, pseudocode, and tests. The results were unsatisfactory, and we identify possible reasons.

[This abstract was generated with the help of AI]

CAAL ; Verification ; FIxed-Point ; Dependency Graph ; Semantics ; CCS ; HML ; Bisimulation ; Games ; Equivalence ; Collapse ; Parallel ; on-the-fly

Download
View record in AAU Student Projects