Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

1990 ◽  
Vol 2 (1) ◽  
pp. 226-246 ◽  
Author(s):  
Xudong He ◽  
John A. N. Lee
Keyword(s):  
Temporal Logic ◽  
Concurrent Systems ◽  
First Order ◽  
Specification And Verification

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

scholarly journals Dynamic Linear Time Temporal Logic

1997 ◽  
Vol 4 (8) ◽  
Author(s):  
Jesper G. Henriksen ◽  
P. S. Thiagarajan
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Order Theory ◽  
Simple Extension ◽  
Propositional Dynamic Logic ◽  
First Order ◽  
Time Semantics ◽  
Linear Time Temporal Logic ◽  
Obvious Manner

A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.

Sign in / Sign up

Export Citation Format

Share Document