PREDICATE TRANSFORMERS FOR REASONING ABOUT CONCURRENT COMPUTATION

被引:15
|
作者
CHANDY, KM
SANDERS, BA
机构
[1] ETH ZURICH,ETH ZENTRUM,INST COMP SYST,CH-8092 ZURICH,SWITZERLAND
[2] CALTECH,PASADENA,CA 91125
关键词
Concurrent programs - Predicate calculus - Predicate transformers - Reasoning - Sequential programs;
D O I
10.1016/0167-6423(94)00033-B
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In this paper we propose a calculus for reasoning about concurrent programs inspired by the wp calculus for reasoning about sequential programs. The calculus uses a small set of familiar rules for dealing with safety, progress and parallel composition. A contribution of this paper is to demonstrate how predicate calculus in general, and predicate transformers in particular, can be used to reason about concurrent programs in which fairness plays a critical role.
引用
收藏
页码:129 / 147
页数:19
相关论文
共 50 条
  • [31] TEMPORAL PREDICATE TRANSFORMERS AND FAIR TERMINATION
    MORRIS, JM
    ACTA INFORMATICA, 1990, 27 (04) : 287 - 313
  • [32] Reasoning about Equilibria in Game-Like Concurrent Systems
    Gutierrez, Julian
    Harrenstein, Paul
    Wooldridge, Michael
    FOURTEENTH INTERNATIONAL CONFERENCE ON THE PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2014, : 408 - 417
  • [33] Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
    Fu, Ming
    Zhang, Yu
    Li, Yong
    THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 233 - 240
  • [34] Reasoning about Concurrent Actionsin Multi-Agent Systems
    樊晓聪
    徐殿祥
    侯建民
    郑国梁
    Journal of Computer Science and Technology, 1999, (04) : 422 - 428
  • [35] A temporal logic for reasoning about timed concurrent constraint programs
    de Boer, FS
    Gabbrielli, M
    Meo, MC
    EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 227 - 233
  • [36] Representing and reasoning about concurrent actions with abductive logic programs
    Li, RW
    Pereira, LM
    ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 1997, 21 (2-4) : 245 - 303
  • [37] Reasoning about nondeterministic and concurrent actions: A process algebra approach
    Chen, XJ
    De Giacomo, G
    ARTIFICIAL INTELLIGENCE, 1999, 107 (01) : 63 - 98
  • [38] Representing and reasoning about concurrent actions with abductive logic programs
    Renwei Li
    Luís Moniz Pereira
    Annals of Mathematics and Artificial Intelligence, 1997, 21 : 245 - 303
  • [39] Reasoning about nondeterministic and concurrent actions: A process algebra approach
    De Giacomo, G
    Chen, XJ
    PROCEEDINGS OF THE THIRTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE AND THE EIGHTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE, VOLS 1 AND 2, 1996, : 658 - 663
  • [40] Reasoning about equilibria in game-like concurrent systems
    Gutierrez, Julian
    Harrenstein, Paul
    Wooldridge, Michael
    ANNALS OF PURE AND APPLIED LOGIC, 2017, 168 (02) : 373 - 403