A tableau calculus for first-order branching time logic

AbstractIn Ockhamist branching-time logic [Prior 67], formulas are meant to be evaluated on a specified branch, or history, passing through the moment at hand. The linguistic counterpart of the manifoldness of future is a possibility operator which is read as ‘at some branch, or history (passing through the moment at hand)’. Both the bundled-trees semantics [Burgess 79] and the 〈moment, history〉 semantics [Thomason 84] for the possibility operator involve a quantification over sets of moments. The Ockhamist frames are (3-modal) Kripke structures in which this second-order quantification is represented by a first-order quantification. The aim of the present paper is to investigate the notions of modal definability, validity, and axiomatizability concerning 3-modal frames which can be viewed as generalizations of Ockhamist frames.

Download Full-text

The decision problem for branching time logic

Journal of Symbolic Logic ◽

10.2307/2274321 ◽

1985 ◽

Vol 50 (3) ◽

pp. 668-681 ◽

Cited By ~ 33

Author(s):

Yuri Gurevich ◽

Saharon Shelah

Keyword(s):

Decision Problem ◽

Companion Paper ◽

Order Theory ◽

Branching Time ◽

First Order ◽

First Order Theory ◽

Time Logic

AbstractThe theory of trees with additional unary predicates and quantification over nodes and branches embraces a rich branching time logic. This theory was reduced in the companion paper to the first-order theory of binary, bounded, well-founded trees with additional unary predicates. Here we prove the decidability of the latter theory.

Download Full-text

Constructing weak simulations from linear implications for processes with private names

Mathematical Structures in Computer Science ◽

10.1017/s0960129518000452 ◽

2019 ◽

Vol 29 (8) ◽

pp. 1275-1308 ◽

Cited By ~ 1

Author(s):

Ross Horne ◽

Alwen Tiu

Keyword(s):

Expressive Power ◽

Dual Pair ◽

Proof System ◽

Branching Time ◽

First Order ◽

Order Extension

AbstractThis paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a ‘left proof’ to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

Download Full-text