A Logical Process Calculus

Abstract

This paper presents the Logical Process Calculus (LPC), a formalism that supports heterogeneous system specifications containing both operational and declarative subspecifications. Syntactically, LPC extends Milner's Calculus of Communicating Systems with operators from the alternation-free linear- time (mu)-calculus (LT(mu)). Semantically, LPC is equipped with a behavioral preorder that generalizes Hennessy's and DeNicola's must-testing preorder as well as LT(mu)'s satisfaction relation, while being compositional for all LPC operators. From a technical point of view, the new calculus is distinguished by the inclusion of (i) both minimal and maximal fixed-point operators and (ii) an unimplementability predicate on process terms, which tags inconsistent specifications. The utility of LPC is demonstrated by means of an example highlighting the benefits of heterogeneous system specification.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 2002
Accession Number
ADA406830

Entities

People

  • Gerald Luttgen
  • Rance Cleaveland

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Calculus
  • Classification
  • Coding
  • Computations
  • Computer Science
  • Databases
  • Electronic Mail
  • Engineers
  • Inclusions
  • Language
  • New York
  • Notation
  • Software Development
  • Space Sciences
  • Specifications
  • Standards
  • Unidirectional

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.