#### Title

Adding the modal mu-calculus to the instruction-set process calculus

#### Date of Award

2005

#### Degree Type

Dissertation

#### Degree Name

Doctor of Philosophy (PhD)

#### Department

Electrical Engineering and Computer Science

#### Advisor(s)

Shiu-Kai Chin

#### Second Advisor

Susan Older

#### Keywords

Mu-calculus, Instruction-set process calculus, Temporal logic, Process algebra

#### Subject Categories

Computer Engineering | Computer Sciences | Electrical and Computer Engineering | Engineering | Physical Sciences and Mathematics

#### Abstract

IspCal is a formal language well suited for describing synchronous digital systems, and it supports hardware composition. It is also a calculus with which we can equate one description with another. However, its original description lacked the ability to express crucial temporal properties of systems, such as safety and liveness.

To provide the ability of expressing temporal properties, we have added a temporal logic (the modal mu-calculus) to IspCal. By adding the modal mu-calculus to IspCal, we enriched the expressiveness of IspCal so that we can express safety-critical temporal properties of systems and verify that systems satisfy the properties. In addition we proved an important proposition of the modal mu-calculus, the satisfaction-equivalence proposition. This proposition states that bisimilar processes share the same properties. The result is a potential great savings in time and effort for property checking.

In this thesis we focus on the procedures for adding the modal mu-calculus to Isp-Cal. We implement the syntax and semantics of the modal mu-calculus as conservative extensions to the Higher Order Logic (HOL4) theorem prover. We also prove several propositions of modal mu-calculus in HOL, such as the satisfaction-equivalence proposition.

#### Access

Surface provides description only. Full text is available to ProQuest subscribers. Ask your Librarian for assistance.

#### Recommended Citation

Min, Byoung Woo, "Adding the modal mu-calculus to the instruction-set process calculus" (2005). *Electrical Engineering and Computer Science - Dissertations*. 60.

https://surface.syr.edu/eecs_etd/60

http://libezproxy.syr.edu/login?url=http://proquest.umi.com/pqdweb?did=921039371&sid=1&Fmt=2&clientId=3739&RQT=309&VName=PQD