=Paper=
{{Paper
|id=Vol-1955/staf-ds-2017-5
|storemode=property
|title=Rule Formats for Nominal Modal Transition Systems
|pdfUrl=https://ceur-ws.org/Vol-1955/staf-ds-2017-5.pdf
|volume=Vol-1955
|authors=Anke Stüber
}}
==Rule Formats for Nominal Modal Transition Systems==
https://ceur-ws.org/Vol-1955/staf-ds-2017-5.pdf
Rule Formats for
Nominal Modal Transition Systems ?
Anke Stüber
Universitet Uppsala, Uppsala, Sweden
anke.stuber@it.uu.se
Abstract. Modal transition systems are specification languages that al-
low the expression of loose specifications. They can model a development
process where an initially partial specification is stepwise refined until
an implementation is obtained. We propose to generalize modal tran-
sition systems to a nominal setting to facilitate the handling of names
and binders as encountered in name-passing process calculi. We need to
show compositionality of the refinement relation. Beyond that we want
to further generalize this idea by compiling SOS rule formats that ensure
compositionality. The results of this research should give a general spec-
ification language where proofs of the theory carry over to other process
calculi expressible in our framework.
1 Problem
In the networked world of today, concurrent communicating systems are ubiq-
uitous. As such systems are complex, we need formal methods to reason about
their properties. When developing software we want to start with a specification
of the intended behavior of the system that we can later use to check whether our
implementation meets the requirements. Process calculi [6, 7] based on labelled
transition systems can be used for specification and modeling of concurrent com-
municating systems.
With process calculi, the languages for specification and implementation of a
system are the same. Bisimulation is used to check the correctness of an imple-
mentation according to a specification. As bisimulation is an equivalence, this
limits the set of possible implementations to a single equivalence class. This
means that contrary to a real-world development process all behavior must al-
ready be defined in the initial specification. Furthermore for the specification of
a system composed of several components it is necessary to specify all behavior
of the components, even the behavior that is only internally visible. We want to
describe a development process where it is possible to refine the specification of
a system by refining the specification of one of its components, as illustrated in
Figure 1.
?
Initial stage of research, supervised by Joachim Parrow
Fig. 1. A refinement step
Modal transition systems [5] are labelled transition systems that have both
may and must transitions, which can be used to describe the necessary and
admissible behavior of a system. This allows for coarser partial specifications
that can be refined by either changing a may into a must transition or removing
a may transition from the system. When no more may transitions are present an
implementation is reached. For checking the correctness of a refined specification
a refinement relation is used. In contrast to the bisimulation equivalence this
relation is not an equivalence but a preorder. This makes the correctness check
easier in practice.
Name-passing process calculi such as the Pi calculus [7] make use of name
generation and scope opening. Names can be scoped to represent local resources.
A locally bound name b that is exported over a channel a in the transition
ā(νb) ā(νc)
P −−−→ P 0 can undergo α-conversion. This leads to the the transition P −−−→
P 0 {c/b} which we want to regard as α-equivalent for each fresh name c. In manual
proofs this kind of problem is often treated only informally. Nominal logic [13]
strictly formalizes notions of renaming via name-swapping and freshness. We
want to generalize the concept of modal transition systems to a name-passing
setting, using nominal logic to simplify the handling of names, binders and α-
equivalence.
An important property of a specification language is compositionality: The
problem of checking the correctness of a complete system according to a specifica-
tion should be decomposable into the simpler problems of checking correctness
of the components. For process calculi, bisimulation preserved by the process
operators fulfills compositionality [5]. For our proposed nominal modal transi-
tion systems we therefore need to investigate whether our refinement relation
is preserved by operators such as the parallel composition operator. For modal
transition systems, when there are no may transitions, refinement coincides with
strong bisimilarity. When there are no must transitions, it coincides with simu-
lation. This brings up the question of whether we can find similar relations in
the nominal setting.
The area of specification languages is large and there are many papers intro-
ducing new languages. Each time the underlying theory such as compositionality
has to be proved again. Rule formats [8] are syntactic restrictions on rules for
operational semantics that guarantee some desirable properties of the semantics
induced by any transition system following the formats. We propose research on
rule formats for a general specification language based on nominal modal tran-
sition systems that ensure compositionality. Such rule formats would eliminate
the need to prove repeatedly the theory for all specification languages that can
be expressed through an instance of the rules.
2 Related Work
The process calculus concept was first introduced by Milner in his work on the
Calculus of Communicating Systems [6]. Process calculi provide a formal model
for reasoning about the behavior and communication of processes. Equivalences
between processes can be described in terms of bisimulation. Milner, Parrow
and Walker generalize this concept with their Pi-calculus [7] in which processes
are allowed to communicate channel names over the communication channels,
making it possible to describe dynamic network structures.
In [5] and [4] Larsen and Thomsen argue that process calculi are ill-suited as
specification languages, since they limit the set of possible implementations for a
specification to a single equivalence class. They propose a specification language
in the form of a labelled transition system with may and must transitions and
a refinement relation between specifications.
Process calculi and specification languages rely on the concepts of names and
binders. Pitts introduced nominal logic [13] to facilitate the reasoning about α-
conversion, freshness and permutation of names. This theory was incorporated
into the interactive theorem prover Isabelle [10] with the definitional extension
Nominal Isabelle [3, 15] which supports binding multiple names at once. Other
frameworks for reasoning about formal semantics such as Twelf [11] and Bel-
uga [12] make use of higher-order abstract syntax to handle names and binders
formally.
For process calculi where terms are elements of arbitrary nominal sets Parrow
et al. [9] define nominal transition systems and introduce a modal logic that can
be used to express bisimulation equivalence by testing whether two processes
satisfy the same set of formulas. We will use this paper and its formalization in
Nominal Isabelle as a starting point for our research, but unlike this approach
start with modal transition systems and generalize them to a nominal setting.
Structural operational semantics (SOS) was first presented by Plotkin in [14]
as a structured method to define rules for operational semantics. The idea was
widely adopted and extended by the concept of rule formats [8] that guarantee
semantic properties by imposing restrictions on the syntax of such rules. Rule
formats for name-passing process calculi ensuring that open bisimilarity is a
congruence have been studied in [2] by means of category theory and in [16]
using the higher-order proof system fold-nabla. Cimini et al. define a framework
based on nominal logic for handling names in SOS in [1].
3 Proposed Solution
We propose to combine the concepts of modal transition systems and nominal
logic to define a specification language that improves the handling of names and
binders as used in name-passing process calculi. This will give us the flexibility of
modal transition systems on top of a rigorous theory for reasoning about objects
depending on names. It will allow the expression of the behavior of a system
in the style of name-passing process algebras while facilitating the refinement
of its specification through the use of may and must transitions as found in
modal transition systems. We need to define a refinement relation and prove
compositionality with the parallel and other process operators. Furthermore we
propose to generalize our specification language by finding SOS rule formats such
that compositionality holds. We will find encodings of existing process algebras
into instances of our rules, eliminating the need to repeat the proofs in each
expressible instance.
To increase the confidence in our proofs we will formalize part of our theory
in the interactive theorem prover Isabelle. In particular, we will rely on the def-
initional extension Nominal Isabelle, providing convenient measures of handling
names and binders.
4 Preliminary Work
My research on this topic is still in the initial stage. I have conducted a literature
survey on process calculi and modal transition systems. In earlier work I gained
experience with proofs on properties of bisimulation, notably in a nominal set-
ting. Furthermore, I have had some practice in formalizing proofs in Nominal
Isabelle.
5 Expected Contributions
The expected contributions of this research are as follows:
– definition of a specification language using nominal transition systems with
modal may and must transitions, a satisfaction relation and a notion of
refinement that allows composition with logical and process operators,
– proofs that our specification language fulfills compositionality with operators
such as the parallel operator and comparisons of our refinement relation with
existing forms of bisimulation,
– methods for checking refinement of specifications,
– generalization of the concept through rule formats that ensure composition-
ality,
– applications of our framework by means of encodings of existing process
algebras1 ,
– formalization of some of the proofs in the interactive theorem prover Isabelle.
This research will generalize nominal process algebras to allow the expression
of loose specifications that can be refined stepwise. Our specification language
will simplify the task of verification for systems that are composed of several
1
exactly which process algebras is not set yet
components because of compositionality: It will permit to check the correctness
of a refinement step by reducing the test to a correctness check of the refined
component. Furthermore, by describing a set of rule formats that ensure com-
positionality this research will be applicable to various existing process algebras
while the desired properties need to be proved only once in the general frame-
work. The proofs written in the theorem prover Isabelle can be reused for process
algebras that can be expressed as instances of our rule formats.
6 Plan for Validation and Evaluation
A large part of this research will deal with the theoretical reasoning about fea-
tures of our proposed rule formats for nominal modal transition systems. To
validate that our framework meets the requirements, we will give proofs for the
desired properties such as compositionality. We will formalize part of our proofs
in Nominal Isabelle to achieve a high confidence in their correctness. Furthermore
we will investigate how our specification language can be used in combination
with existing tools for model checking.
The advantage of our modal specification language with refinement over ap-
proaches using bisimulation can be assessed through performance tests of tools
that verify the correctness of an implementation according to a specification
when components of a partial implementation are refined. As for the general
framework of rule formats we will evaluate its usefulness by encoding existing
process calculi in it. For the process calculi we can encode this way the the-
oretical results will carry over, eliminating the need for new proofs for every
expressible calculus.
7 Current Status
Currently I am taking a course on interactive theorem proving in Isabelle to
increase my knowledge in that area. Moreover, I am taking a course on cate-
gory theory that is expected to help with the understanding of papers that use
category theory as a means of reasoning about rule formats. As a next step I
will conduct a literature survey on structural operational semantics for nominal
process algebras. In Swedish universities it is common to write a thesis for a
Licentiate degree after completion of half of the studies for a PhD. In this thesis
I plan to include the definition of a nominal modal specification language, proofs
of its properties such as compositionality, methods for refinement checking and
the formalization of the definitions in Nominal Isabelle, due by fall 2018. Subse-
quently I will work on generalizing the results through rule formats, applications
and further formal proofs in Nominal Isabelle for inclusion into the PhD thesis.
I expect to finish in 2021.
References
[1] M. Cimini, M. R. Mousavi, M. A. Reniers, and M. J. Gabbay. “Nominal
SOS”. In: Electronic Notes in Theoretical Computer Science 286 (2012),
pp. 103–116.
[2] M. Fiore and S. Staton. “A congruence rule format for name-passing pro-
cess calculi”. In: Information and Computation 207.2 (2009), pp. 209–236.
[3] B. Huffman and C. Urban. “A New Foundation for Nominal Isabelle”.
In: 1st International Conference on Interactive Theorem Proving – ITP
’10. Ed. by M. Kaufmann and Paulson L. C. Vol. 6172. Lecture Notes in
Computer Science. Berlin a.o.: Springer, 2010, pp. 35–50.
[4] K. G. Larsen. “Modal Specifications”. In: Automatic Verification Methods
for Finite State Systems. Ed. by J. Sifakis. Vol. 407. Lecture Notes in
Computer Science. Berlin a.o.: Springer, 1989, pp. 232–246.
[5] K. G. Larsen and B. Thomsen. “A Modal Process Logic”. In: 3rd Annual
Symposium on Logic in Computer Science – LICS ’88. Washington a.o.:
IEEE Computer Society, 1988, pp. 203–210.
[6] R. Milner. “A Calculus of Communicating Systems”. In: vol. 92. Lecture
Notes in Computer Science. Berlin a.o.: Springer, 1980.
[7] R. Milner, J. Parrow, and D. Walker. “A Calculus of Mobile Processes, I”.
In: Information and Computation 100.1 (1992), pp. 1–40.
[8] M. R. Mousavi, M. A. Reniers, and J. F. Groote. “SOS formats and meta-
theory: 20 years after”. In: Theoretical Computer Science 373.3 (2007),
pp. 238–272.
[9] J. Parrow, J. Borgström, L.-H. Eriksson, R. Gutkovas, and T. Weber.
“Modal Logics for Nominal Transition Systems”. In: 26th International
Conference on Concurrency Theory – CONCUR ’15. Ed. by L. Aceto and
D. de Frutos Escrig. Vol. 42. Leibniz International Proceedings in Infor-
matics. Wadern: Leibniz-Zentrum für Informatik, 2015, pp. 198–211.
[10] L. C. Paulson. Isabelle – A Generic Theorem Prover. Vol. 828. Lecture
Notes in Computer Science. Berlin a.o.: Springer, 1994.
[11] F. Pfenning and C. Schürmann. “System Description: Twelf – A Meta-
Logical Framework for Deductive Systems”. In: Proceedings of the 16th
International Conference on Automated Deduction – CADE-16. Ed. by H.
Ganzinger. Vol. 1632. Lecture Notes in Artificial Intelligence. Berlin a.o.:
Springer, 1999, pp. 202–206.
[12] B. Pientka and J. Dunfield. “Beluga: A Framework for Programming and
Reasoning with Deductive Systems (System Description)”. In: Proceedings
of the 5th International Conference on Automated Reasoning – IJCAR
’10. Ed. by J. Giesl and R. Hähnle. Vol. 6173. Lecture Notes in Computer
Science. Berlin a.o.: Springer, 2010, pp. 15–21.
[13] A. M. Pitts. “Nominal Logic: A First Order Theory of Names and Bind-
ing”. In: Theoretical Aspects of Computer Software: 4th International Sym-
posium. Ed. by N. Kobayashi and B. C. Pierce. Vol. 2215. Lecture Notes
in Computer Science. Berlin a.o.: Springer, 2001, pp. 219–242.
[14] G. D. Plotkin. A Structural Approach to Operational Semantics. Technical
Report DAIMI FN-19. Aarhus: Computer Science Department, Aarhus
University, 1981.
[15] C. Urban and C. Kaliszyk. “General Bindings and Alpha-Equivalence in
Nominal Isabelle”. In: Logical Methods in Computer Science 8.2 (2012),
pp. 1–35.
[16] A. Ziegler, D. Miller, and C. Palamidessi. “A Congruence Format for Name-
passing Calculi”. In: Electronic Notes in Theoretical Computer Science
156.1 (2006), pp. 169–189.