Operational and Denotational Properties of a Modal Process Logic
Author
Huttel, Hans
Term
4. term
Education
Publication year
2012
Abstract
Dette arbejde udvikler teorien for en modal proceslogik, først introduceret af Kim Larsen og Bent Thomsen, til at beskrive og sammenligne adfærd i systemer med samtidige processer. Logikken kan ses som en udvidelse af CCS (Calculus of Communicating Systems). Vi giver en operationel semantik, dvs. trin-for-trin regler for, hvordan processer kan opføre sig, og bruger den til at definere en præorden på logikkens formler (en måde at sige, at én formel er mindst lige så informativ som en anden). Vi undersøger også en denotationel beskrivelse, oprindeligt foreslået af Larsen og Thomsen, og viser i hvilket omfang en raffineringsorden (hvor én specifikation er en mere detaljeret udgave af en anden) forklarer den orden, som den denotationelle semantik introducerer. Særligt viser vi, at den modale proceslogik semantisk omfatter sproget for partielle specifikationer, som de også introducerede. Vi udvider logikken med CCS’ statiske konstruktioner (strukturelle byggesten til at kombinere systemer) og introducerer en ny observationspræorden, som vi anvender på tre eksempler. Endelig præsenterer vi bevissystemer, der er sunde (beviser kun sande udsagn) og fuldstændige (kan bevise alle sande udsagn) for både den stærke raffineringsorden og den lighed, der er defineret af den denotationelle semantik.
This thesis develops the theory of a modal process logic, originally introduced by Kim Larsen and Bent Thomsen, for describing and comparing the behavior of concurrent, communicating systems. The logic can be viewed as an extension of CCS (Calculus of Communicating Systems). We give an operational semantics (step-by-step rules for how processes can behave) and use it to define a preorder on formulas in the logic (a way to say that one formula is at least as informative as another). We also examine a denotational description, originally proposed by Larsen and Thomsen, and show how a refinement ordering (one specification being a more detailed version of another) accounts for the ordering induced by that semantics. In particular, we show that the modal process logic semantically subsumes the language of partial specifications that they also introduced. We add the static constructs of CCS (structural building blocks for composing systems) to the logic and introduce a new observational preorder, which we apply to three examples. Finally, we provide proof systems that are sound (prove only true statements) and complete (can prove all true statements) for the strong refinement ordering and for equality as defined by the denotational semantics.
[This abstract was generated with the help of AI]
Documents