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.

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

Link to Full Text

Share

COinS