We examine modal and temporal logics for processes. In section 1 we introduce concurrent
processes as terms of an algebraic language comprising a few basic operators, as …

We survey principles of model checking techniques for the automatic analysis of reactive
systems. The use of model checking is exemplified by an analysis of the Needham …

Abstract Model checking is an automatic technique for verifying finite-state reactive systems,
such as sequential circuit designs and communication protocols. Specifications are …

A central aim and ever-lasting dream of computer science is to put the development of
hardware and software systems on a mathematical basis which is both firm and practical …

The subject of this chapter is the study of formal languages (mostly languages recognizable
by finite automata) in the framework of mathematical logic. The connection between …

Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided
reasoning system ACL2 can be used in productive and innovative ways to design, build, and …

We observe that the problem of deciding the winner in mean payoff games is in the
complexity class UP∩ co-UP. We also show a simple reduction from parify games to mean …

Translating linear temporal logic formulas to automata has proven to be an effective
approach for implementing linear-time model-checking, and for obtaining many extensions …

In this paper we develop a new algorithm for deciding the winner in parity games, and hence
also for the modal μ-calculus model checking. The design and analysis of the algorithm is …

The Μ-calculus can be viewed as essentially the “ultimate” program logic, as it expressively
subsumes all propositional program logics, including dynamic logics, process logics, and …