Process logic with regular formulas
type: Item
instance of: scholarly article
title: Process logic with regular formulas
zbMATH Open document ID: 0572.03010
DOI: 10.1016/0304-3975(85)90225-7
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: The reviewer [Acta Inf. 14, 359-369 (1980; Zbl 0423.68005)] proposed that dynamic logic invented by V. R. Pratt and temporal logic exploited for computer science by A. Pnueli and his school should be combined to yield the right process logic. In response to this suggestion, \textit{D. Harel, D. Kozen} and \textit{R. Parikh} [J. Comput. Syst. Sci. 25, 144-170 (1982; Zbl 0494.03016)] succeeded in presenting a decidable propositional process logic of a natural axiomatization. Keeping this line, the authors have made a great step toward the right process logic by using the operators chop and slice instead of f and suf. Most of the technical discussion here is devoted to showing that this new logic is more expressive than the formerly proposed one.
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3912351
zbMATH Keywords: regular expressions
zbMATH Keywords: complete axiomatization
zbMATH Keywords: decidable propositional process logic
zbMATH Keywords: chop
zbMATH Keywords: slice
author: David Harel
author: David Peleg
reviewed by: Hirokazu Nishimura
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90225-7
OpenAlex ID: W2044206530
cites work: Q4065051
cites work: Q4094352
cites work: Theories of automata on \(\omega\)-tapes: a simplified approach
cites work: Algorithmic properties of structures
cites work: Q5584402
cites work: Propositional dynamic logic of regular programs
cites work: Q4343990
cites work: Two results on process logic
cites work: Recurring Dominoes: Making the Highly Undecidable Highly Understandable
cites work: Process logic: Expressiveness, decidability, completeness
cites work: An axiomatic basis for computer programming
cites work: An elementary proof of the completeness of PDL
cites work: Q4124327
cites work: Descriptively complete process logic
cites work: Q5596237
cites work: The complexity of propositional linear temporal logics
cites work: Is the Interesting Part of Process Logic uninteresting?: A Translation from PL to PDL
cites work: Star-free regular sets of ω-sequences
cites work: Temporal logic can be more expressive
Recommended article: Equations between Regular Terms and an Application to Process Logic
Recommended article: Flow logic for process calculi
Recommended article: A logical process calculus
Recommended article: Coverability Synthesis in Parametric Petri Nets
Recommended article: Q4972733
Recommended article: Dynamic process logic
Recommended article: Q3343422
Recommended article: Logic program forms
Recommended article: Q3341881
Recommended article: Q4260381
description: scientific article; zbMATH DE number 3912351