scholarly journals Propositional Dynamic Logic with Storing, Recovering and Parallel Composition

2011 ◽  
Vol 269 ◽  
pp. 95-107 ◽  
Author(s):  
Mario R.F. Benevides ◽  
Renata de Freitas ◽  
Petrucio Viana
Keyword(s):  
Dynamic Logic ◽  
Parallel Composition ◽  
Propositional Dynamic Logic

scholarly journals A Dynamic Epistemic Logic with Finite Iteration and Parallel Composition

2021 ◽  
Author(s):  
Andreas Herzig ◽  
Frédéric Maris ◽  
Elise Perrotin
Keyword(s):  
Epistemic Logic ◽  
Dynamic Logic ◽  
Dynamic Epistemic Logic ◽  
Finite Horizon ◽  
Parallel Composition ◽  
Propositional Dynamic Logic ◽  
Restricted Version ◽  
Standard Program

Existing dynamic epistemic logics combine standard epistemic logic with a restricted version of dynamic logic. Instead, we here combine a restricted epistemic logic with a rich version of dynamic logic. The epistemic logic is based on `knowing-whether' operators and basically disallows disjunctions and conjunctions in their scope; it moreover captures `knowing-what'. The dynamic logic has not only all the standard program operators of Propositional Dynamic Logic, but also parallel composition as well as an operator of inclusive nondeterministic composition; its atomic programs are assignments of propositional variables. We show that the resulting dynamic epistemic logic is powerful enough to capture several kinds of sequential and parallel planning, and so both in the unbounded and in the finite horizon version.

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