scientific article; zbMATH DE number 1142324
From MaRDI portal
Publication:4385540
zbMath0900.68306MaRDI QIDQ4385540
Publication date: 14 May 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (38)
A formalization of programs in first-order logic with a discrete linear order ⋮ Stratified least fixpoint logic ⋮ Rabin tree automata and finite monoids ⋮ On dynamic algebras ⋮ Canonical finite models of Kleene algebra with tests ⋮ Ultraproducts and possible worlds semantics in institutions ⋮ The complexity of PDL with interleaving ⋮ Actors, actions, and initiative in normative system specification ⋮ Propositional dynamic logic with recursive programs ⋮ An infinite pebble game and applications ⋮ Free choice and contextually permitted actions ⋮ First order data types and first order logic ⋮ Fixed point characterization of infinite behavior of finite-state systems ⋮ Non-terminating processes in the situation calculus ⋮ Exponential improvement of time complexity of model checking for multiagent systems with perfect recall ⋮ Mathematical modal logic: A view of its evolution ⋮ A specification structure for deadlock-freedom of synchronous processes ⋮ Path constraints in semistructured data ⋮ On models for propositional dynamic logic ⋮ On the expressive power of finitely typed and universally polymorphic recursive procedures ⋮ On the logic of UNITY ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ Tableaux and algorithms for Propositional Dynamic Logic with Converse ⋮ A natural deduction approach to dynamic logic ⋮ Proof-theoretic notions for software maintenance ⋮ Tableaux for constructive concurrent dynamic logic ⋮ Regular database update logics ⋮ Model checking propositional dynamic logic with all extras ⋮ Constructive modal logics. I ⋮ Clausal Tableaux for Hybrid PDL ⋮ On the power of built-in relations in certain classes of program schemes ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ Model checking for hybrid logic ⋮ EXPtime tableaux for ALC ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL. ⋮ On the completeness of propositional Hoare logic ⋮ Complexity analysis of propositional concurrent programs using domino tiling ⋮ Program schemes, arrays, Lindström quantifiers and zero-one laws
This page was built for publication:
