scientific article; zbMATH DE number 1556014

Jerzy Tiuryn, David Harel, Dexter Kozen

Publication date: 24 January 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General logic (03Bxx)

Related Items (only showing first 100 items - show all)

Distributed Adaptive Systems ⋮ Concurrent Dynamic Algebra ⋮ Differential Game Logic ⋮ The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Relational Differential Dynamic Logic ⋮ Branching-time logics and fairness, revisited ⋮ THE LOGIC OF RESOURCES AND CAPABILITIES ⋮ Modelling phenomena and dynamic logic of phenomena ⋮ Representing any-time and program-iteration by infinitary conjunction ⋮ Separation logics and modalities: a survey ⋮ Propositional quantification in logics of contingency ⋮ Reasoning as Speech Acts ⋮ To be announced ⋮ A Qualitative Theory of Cognitive Attitudes and their Change ⋮ Metric dynamic equilibrium logic ⋮ A specification logic for programs in the probabilistic guarded command language ⋮ Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect ⋮ A dynamic logic with branching modalities ⋮ Weighted Linear Dynamic Logic ⋮ A modal loosely guarded fragment of second-order propositional modal logic ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ On the complexity of Kleene algebra with domain ⋮ Can we communicate? Using dynamic logic to verify team automata ⋮ Smooth coalgebra: testing vector analysis ⋮ Practical coinduction ⋮ On Groenendijk and Stokhof’s “Dynamic Predicate Logic” ⋮ A short introduction to SHACL for logicians ⋮ From Gödel's incompleteness theorem to the completeness of bot beliefs (extended abstract) ⋮ From post-conditions to post-region invariants ⋮ Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems ⋮ Unnamed Item ⋮ Towards Metric Temporal Answer Set Programming ⋮ Completeness of ASM Refinement ⋮ A logic for metric and topology ⋮ Structures of Oppositions in Public Announcement Logic ⋮ Common Knowledge Logic in a Higher Order Proof Assistant ⋮ Dynamic Semantics of Plurals DPL ⋮ Propositional Dynamic Logic with Program Quantifiers ⋮ Deontic Logic, Contrary to Duty Reasoning and Fault Tolerance ⋮ Verification by Parallelization of Parametric Code ⋮ Halting and Equivalence of Program Schemes in Models of Arbitrary Theories ⋮ Propositional Dynamic Logic with Storing, Recovering and Parallel Composition ⋮ KeY: A Formal Method for Object-Oriented Systems ⋮ Terminating Tableaux for Hybrid Logic with Eventualities ⋮ A Complete Axiomatic System for a Process-Based Spatial Logic ⋮ A Tableau Calculus for Regular Grammar Logics with Converse ⋮ A Temporal Logic of Normative Systems ⋮ A Complete STIT Logic for Knowledge and Action, and Some of Its Applications ⋮ From Philosophical to Industrial Logics ⋮ Formal Modelling of Emotions in BDI Agents ⋮ Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs ⋮ Towards a Logic for Abstract MetaFinite State Machines ⋮ Axiomatization and computability of a variant of iteration-free PDL with fork ⋮ Decidable Extensions of Hennessy-Milner Logic ⋮ Reasoning in Dynamic Logic about Program Termination ⋮ From Monadic Logic to PSL ⋮ Model Checking Strategic Equilibria ⋮ PDL with intersection and converse: satisfiability and infinite-state model checking ⋮ On the Completeness of Dynamic Logic ⋮ Bounded Relational Analysis of Free Data Types ⋮ Knowledge and Local Actions ⋮ GOAL Agents Instantiate Intention Logic ⋮ $\mathcal{CL}$ : An Action-Based Logic for Reasoning about Contracts ⋮ Abstract Interpretation of Symbolic Execution with Explicit State Updates ⋮ Foundations of RDF Databases ⋮ Unnamed Item ⋮ Segerberg on the Paradoxes of Introspective Belief Change ⋮ 2-Exp Time lower bounds for propositional dynamic logics with intersection ⋮ Verification of Java Programs with Generics ⋮ Unnamed Item ⋮ Extracting Program Logics From Abstract Interpretations Defined by Logical Relations ⋮ On Diagrams and General Model Checkers ⋮ Approximating bisimilarity for Markov processes ⋮ Logics of informational interactions ⋮ Algebras of modal operators and partial correctness ⋮ Static analysis of navigational XPath over graph databases ⋮ To drive or not to drive: a logical and computational analysis of European transport regulations ⋮ Bisimilar and logically equivalent programs in PDL ⋮ Extending propositional dynamic logic for Petri nets ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Canonical finite models of Kleene algebra with tests ⋮ Logical theories of intention and the database perspective ⋮ Pooling modalities and pointwise intersection: semantics, expressivity, and dynamics ⋮ Deontic action logic, atomic Boolean algebras and fault-tolerance ⋮ Computation as social agency: what, how and who ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Algorithmically broad languages for polynomial time and space ⋮ Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ Propositional dynamic logic with quantification over regular computation sequences ⋮ Logics of communication and change ⋮ Complete axiomatizations for quantum actions ⋮ Specification of systems with parameterised events: An institution-independent approach ⋮ A deductive approach towards reasoning about algebraic transition systems ⋮ Computational inductive definability ⋮ Action negation and alternative reductions for dynamic deontic logics ⋮ A formal model of emotion triggers: an approach for BDI agents ⋮ Abstract representation theorems for demonic refinement algebras ⋮ The dynamic turn in quantum logic ⋮ An observationally complete program logic for imperative higher-order functions

This page was built for publication: