Eliminating disjunctions of leads-to properties
type: Item
instance of: scholarly article
title: Eliminating disjunctions of leads-to properties
zbMATH Open document ID: 0802.68081
DOI: 10.1016/0020-0190(94)90010-8
author: Ken Calvert
published in: Information Processing Letters
publication date: 1994-04-05T00:00:00Z
review text: Leads-to properties allow specification of \textit{progress properties} of reactive programs. We define a predicate transformer, in terms of which finite disjunctions of leads-to properties can be rewritten as equivalent single leads-to properties. Although disjunctions of leads-to properties do not typically arise in progress specifications, we give an example showing how they may be introduced through manipulation of nested implications of leads-to properties; such \textit{nested} implications allow subtle dependencies between a program's progress and that of its environment to be conveniently specified. After introducing the predicate transformer we show how to define a single leads-to property equivalent to a given disjunction of two leads-to properties. An equivalent definition in terms of \textit{unless} properties is given. Finally, we generalize the predicate transformer to any finite number of arguments.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q10
zbMATH DE Number: 540883
zbMATH Keywords: concurrency
zbMATH Keywords: formal semantics
zbMATH Keywords: specification languages
zbMATH Keywords: temporal logic
zbMATH Keywords: UNITY
zbMATH Keywords: formal specifications
zbMATH Keywords: predicate transformer
describes a project that uses: UNITY
MaRDI profile type: Publication
full work available at URL: 0020-0190(94)90010-8
OpenAlex ID: W1964726517
cites work: Q4692502
cites work: Specifying Concurrent Program Modules
cites work: A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
Recommended article: ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION
Recommended article: Eliminating disjunctions by disjunction elimination
Recommended article: Eliminating the fixed predicates from a circumscription
Recommended article: REPRESENTING CONJUNCTIVE DEDUCTIONS BY DISJUNCTIVE DEDUCTIONS
Recommended article: Q2753689
Recommended article: Q3322079
Recommended article: Eliminating negation from normal logic programs
Recommended article: Elimination of Disjunction and Negation in Answer-Set Programs under Hyperequivalence
Recommended article: Linear quantifier elimination
description: scientific article; zbMATH DE number 540883