英语论文网

. . . . . . . . . . . . . . . . . . . . . 18
4.10.1 Pseudo-application . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
4.11 Commitments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2 Intro duction
2.1 Background
The -calculus is a pro cess algebra - a mathematical way of expressing computer programs
(pro cesses).代写留学生论文 It has some expressful "built-in" features, go o d for describing distributed, com-
municating and dynamic computer systems (systems where pro cesses can change over time).
A go o d example is the GSM digital telephone network, where the pro cesses (telephones) can
b e turned on and o , and the telephone can move within the network. This is often referred
to as mobility. A temp oral logic is a language that can express prop erties for pro cesses and
their actions (p ossibly in nitely many { they may run forever). The temp oral logic can de-
scrib e prop erties like "it must always b e p ossible to move the pro cess to another state", (i.e.
the pro cess must never deadlo ck), or "it must react up on every p ossible input", and such
sp eci c b ehaviours. To combine a pro cess, that we wish to control for a certain prop erty,
and a formula, that expresses the prop erty, and calculate whether the formula holds for the
pro cess or not (if the pro cess is a model for the formula) is known as model checking. In this
pap er, we will present an algorithm for a mo del checker, The Model Prover, for checking a
sp eci c class of -calculus-pro cesses (" nite control agents") against a formula, as expressed
in the temp oral logic known as the modal -calculus.

References
1] Trollkarlen Blir Ingenjor - Formella Meto der: En Oversikt
Joachim Parrow
KTH Sto ckholm, Sweden May 1997
https://www.sics.se/~joachim/hattext.ps.Z
Shorter version also published as "Programmeraren som Shaman",
Forskning & Framsteg #2, february 1998
https://www.fof.se/artiklar/98 2 14.htm
2] Foundational Calculi For Programming Languages
(To App ear In The CRC Handb o ok of Computer Science and Engineering)
Benjamin C. Pierce
Computer Lab oratory, University of Cambridge, UK, decemb er 1995.
3] Berakningsbarhet for dataloger: Fran till P
Kent Petersson
Programmeringsmeto dikgrupp en,
Inst. f. Informationsb ehandling, Goteb orgs Universitet/Chalmers
Bokforlagethttps://www.51lunwen.org/liuxuelunwendx/ Aquila 1987/1988.
4] Mathematical Foundations of Programming
Frank S. Beckman
Bro oklyn College of the City University of New York
The System Programming Series, Addison-Wesley 1980
5] Intro duction to Combinators and -calculus
J. Roger Hindley
Dept. of mathematics and Computer Science, University College, Swansea
Jonathan P. Selldin
Dept. of Mathematics, Concordia University, Montreal
London Mathematical So ciety Student Texts 1
Cambridge University Press 1986
6] An Intro duction to Mo dal Logic
G. E. Hughes & M. J. Cresswell
Victoria University of Wellington
Methuen & Co, London 1968
7] The Polyadic -calculus: a Tutorial
Robin Milner
Dept. of Computer Science, University of Edinburgh