Bernhard Steffen

TCS Journal 2008 Journal Article

Preface

• Tiziana Margaria
• Bernhard Steffen

TCS Journal 1999 Journal Article

Model checking the full modal mu-calculus for infinite sequential processes

• Olaf Burkart
• Bernhard Steffen

It is known that pushdown processes have a decidable monadic second-order theory (Muller and Schupp, Theoret. Comput. Sci. 37 (1985) 51–; 75) and that this result covers the model-checking problem for the modal mu-calculus. Unfortunately, the corresponding decidability procedure is not practical due to its nonelementary complexity. Recently, however, a very intricate elementary algorithm for model checking the full modal mu-calculus for pushdown processes based on games was presented by Walukiewicz (CAV'96, Lecture Notes in Computer Science, vol. 1102, Springer, Berlin, 1996, pp. 62–; 74). Lifting the classical finite-state model checking technique to second-order, we develop here a more structural and transparent elementary algorithm for model-checking infinite sequential processes, including context-free processes, pushdown processes, and regular graphs, that captures the full modal mu-calculus as well. Whereas the actual model-checking algorithm simply resorts to backtracking in order to capture alternation, the corresponding correctness proof requires to introduce the stronger framework of dynamic environments which are modelled by finite-state automata.

TACAS Conference 1995 Conference Paper

A constraint oriented proof methodology based on modal transition systems

• Kim G. Larsen
• Bernhard Steffen
• Carsten Weise

MFCS Conference 1995 Conference Paper

An Elementary Bisimulation Decision Procedure for Arbitrary Context-Free Processes

• Olaf Burkart
• Didier Caucal
• Bernhard Steffen

Abstract We present an elementary algorithm for deciding bisimulation between arbitrary context-free processes. This improves on the state of the art algorithm of Christensen, Hüttel and Stirling consisting of two semi-decision procedures running in parallel, which prohibits any complexity estimation. The point of our algorithm is the effective construction of a finite relation characterizing all bisimulation equivalence classes, whose mere existence was exploited for the above mentioned decidability result.

TACAS Conference 1995 Conference Paper

Parallelism for free: Bitvector analyses ⇒ no state explosion!

• Jens Knoop
• Bernhard Steffen
• Jürgen Vollmer

MFCS Conference 1993 Conference Paper

Deciding Testing Equivalence for Real-Time Processes with Dense Time

• Bernhard Steffen
• Carsten Weise

Abstract We present a decision algorithm for testing equivalence of realtime systems with a dense time domain. Real-time systems are modelled by timed graphs, while the decision algorithm uses“ mutually refined” timer region graphs. The mutual refinement is important for the synchronization of the timers of different real-time systems. Key to our decision algorithm is the fact that — despite the dense time domain — testing can be reduced to Π-bisimulation in very much the same way as in the untimed case.

TCS Journal 1991 Journal Article

Finite constants: characterizations of a new decidable set of constants

• Bernhard Steffen
• Jens Knoop

Constant propagation, the replacement of program terms which represent a unique value at run time by their values, is a classical program optimization method. In spite of being treated for years, constant propagation still has been in the unsatisfactory phase of heuristics. We enhance the known constant propagation techniques to obtain an algorithm which is optimal for programs without loops. Fundamental is the introduction of a new decidable set of constants, the finite constants. This set has two different characterizations: a denotational one, which directly specifies our iterative algorithm and an operational one, which delivers the completeness or optimality of this algorithm for programs without loops. The algorithm is implemented in a commercial compiler project.

MFCS Conference 1989 Conference Paper

Finite Constants: Characterizations of a New Decidable Set of Constants

• Bernhard Steffen
• Jens Knoop

Abstract Constant propagation — the replacement of program terms which represent a unique value at run time by their values — is a classical program optimization method. In spite of being treated for years, constant propagation still has been in the unsatisfactory phase of heuristics. We enhance the known constant propagation techniques to obtain an algorithm which is optimal for programs without loops. Fundamental is the introduction of a new decidable set of constants, the finite constants. This set has two different characterizations: a denotational one, which directly specifies our iterative algorithm and an operational one, which delivers the completeness or optimality of this algorithm for programs without loops. The algorithm is implemented in a commercial compiler project.

MFCS Conference 1989 Conference Paper

Optimal Data Flow Analysis via Observational Equivalence

• Bernhard Steffen

Abstract In [18] a three level model was presented to establish a concept of completeness or optimality for data flow analysis algorithms in the framework of abstract interpretation [2]. The notion of observational equivalence introduced here generalizes the idea of the three level model, which can only deal with hierarchies of abstract interpretations. Investigating this more general notion, it actually turns out that the three level model is general in a theoretical sense: it determines the most abstract computation level which delivers complete results. However, consideration of other aspects of data flow analysis profit from the extra generality of our observation directed approach. For example the completeness or optimality proof for a “real life” optimizer could be shortened significantly this way.