NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
A Logical Process CalculusThis 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: (1) both minimal and maximal fixed-point operators and (2) an unimple-mentability 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.
Document ID
20020080693
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Cleaveland, Rance (State Univ. of New York Stony Brook, NY United States)
Luettgen, Gerald (Sheffield Univ. United Kingdom)
Bushnell, Dennis M.
Date Acquired
September 7, 2013
Publication Date
August 1, 2002
Subject Category
Computer Programming And Software
Report/Patent Number
NASA/CR-2002-211759
ICASE-2002-26
NAS 1.26:211759
Funding Number(s)
CONTRACT_GRANT: NSF CCR-99-88489
CONTRACT_GRANT: NAS1-97046
PROJECT: RTOP 505-90-52-01
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available