Temporal Runtime Verification using Monadic Difference Logic (2007)
Andersen, Henrik Reif, Kristoffersen, Kaare J.
In this paper we present an algorithm for performing runtime verification of a bounded temporal logic over timed runs. The algorithm consists of three elements. First, the bounded temporal formula to...
Calculating Valid Domains for BDD-Based Interactive Configuration (2007)
Hadzic, Tarik, Jensen, Rune Moller, Andersen, Henrik Reif
In these notes we formally describe the functionality of Calculating Valid Domains from the BDD representing the solution space of valid configurations. The formalization is largely based on the CLab...
Generic Global Constraints based on MDDs (2007)
Tiedemann, Peter, Andersen, Henrik Reif, Pagh, Rasmus
Constraint Programming (CP) has been successfully applied to both constraint satisfaction and constraint optimization problems. A wide variety of specialized global constraints provide critical...
Interactive Configuration by Regular String Constraints (2006)
Hansen, Esben Rune, Andersen, Henrik Reif
A product configurator which is complete, backtrack free and able to compute the valid domains at any state of the configuration can be constructed by building a Binary Decision Diagram (BDD)....
A Generic Global Constraint based on MDDs (2006)
Tiedemann, Peter, Andersen, Henrik Reif, Pagh, Rasmus
The paper suggests the use of Multi-Valued Decision Diagrams (MDDs) as the supporting data structure for a generic global constraint. We give an algorithm for maintaining generalized arc consistency...
Sur La Verification De La Satisfaction Pour La Logique Des Differences (2003)
Docteur De L'universit, En Informatique, Karem A. Sakallah, Henrik Reif Andersen, Oded Maler, Directeur De These, ...
this document, we may refer to Boolean literals as Booleans and to numerical literals as constraints
Timed Verification of Asynchronous Circuits (2002)
Jesper Mller, Henrik Hulgaard, Henrik Reif Andersen
We describe a methodology for analyzing timed systems symbolically.
Symbolic Model Checking of Timed Guarded Commands using Difference Decision Diagrams (2002)
Jesper Mller, Henrik Hulgaard, Henrik Reif Andersen
We describe a novel methodology for analyzing timed systems symbolically. Given a formula representing a set of states, we describe how to determine a new formula that represents the set of states...
Copyright C, Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard
In this paper we present a method for determining satis ability of formulae represented by Boolean Expression Diagrams. The method uses the Up One algorithm for splitting on variables and rewriting...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (2000)
Jrn Lind-nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kare Kristoffersen, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a new technique that uses compositionality and dependency analysis...
Difference Decision Diagrams (1999)
Jesper Mller, Jakob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard
This paper describes a new data structure, difference decision diagrams (DDDs), for representing a Boolean logic over inequalities of the form x-y
Veri cation of Large State/Event Systems using Compositionality and Dependency Analysis (1999)
Henrik Reif Andersen, Henrik Hulgaard, Gerd Behrmann, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (1999)
Jrn Lind-nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kare Kristoffersen, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Equivalence Checking of Combinational Circuits using Boolean Expression Diagrams (1999)
Henrik Hulgaard, Poul Frederick Williams, Henrik Reif Andersen
The combinational logic-level equivalence problem is to determine whether two given combinational circuits implement the same Boolean function. This problem arises in a number of CAD applications,...
Boolean Expression Diagrams (1999)
Henrik Reif Andersen, Henrik Hulgaard
This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs)...
Distributed Implementation of a CCS-like Programming Language for Embedded Systems (1999)
We introduce a programming language for embedded systems. The language is based on the process algebra pmc which like ccs has concurrent composition of processes and synchronous point-to-point...
PMC: A Programming Language for Embedded Systems (1999)
Simon Mrk, Ken Larsen, Henrik Reif Andersen, Lyngby Danmark, Peter Sestoft
The process algebra pmc (Processes with Multiple Clocks) extends Milner's ccs with a notion of qualitative time called clocks. The algebra has been used for specifying industrial size case-studies....
Local Computation of Simultaneous Fixed-Points (1999)
We present a very simple, yet general algorithm for computing simultaneous, minimum fixed-points of monotonic functions, or turningtheviewpoint slightly, an algorithm for computing minimum solutions...
Henrik Hulgaard, Poul Frederick Williams, Henrik Reif Andersen
The combinational logic-level equivalence problem is to determine whether two given combinational circuits implement the same Boolean function. This problem arises in a number of CAD applications,...
Equivalence Checking of Combinational Circuits using Boolean Expression Diagrams (1999)
Henrik Hulgaard, Poul Frederick Williams, Henrik Reif Andersen
The combinational logic-level equivalence problem is to determine whether two given combinational circuits implement the same Boolean function. This problem arises in a number of CAD applications,...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (1998)
Henrik Reif Andersen, Henrik Hulgaard, Gerd Behrmann, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Boolean Expression Diagrams (1998)
Henrik Reif Andersen, Henrik Hulgaard
This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs)...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (1998)
Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kare Kristoffersen, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (1998)
Jrn Lind-nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kare Kristoffersen, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (1998)
Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kare Kristoffersen, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Verification of Large State/Event Systems using Compositionality and Dependency Analysis (1998)
Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kare Kristoffersen, Kim G. Larsen
. A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to...
Boolean Expression Diagrams (1997)
Henrik Reif Andersen, Henrik Hulgaard
This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs)...
Boolean Expression Diagrams (1997)
Henrik Reif Andersen, Henrik Hulgaard
This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs)...
Boolean Expression Diagrams (1997)
Henrik Reif Andersen, Henrik Hulgaard
This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs)...
Boolean Expression Diagrams (1997)
Henrik Reif Andersen, Henrik Hulgaard
This paper presents a new data structure called Boolean Expression Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs)...
Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion (1997)
. This paper presents an algorithm for solving Boolean fixedpoint equations containing one level of nesting of minimum and maximum fixed points. The algorithm assumes that the equations of the inner...
A Compositional Proof System for the Modal µ-Calculus (1997)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal ¯- calculus. The proof system is compositional in the...
A Process Algebra with Multiple Clocks (1997)
Henrik Reif Andersen, Michael Mendler
In this report we propose a novel approach to the specification of real-time behaviour based on process algebras. In contrast to the usual pattern, involving a fixed, measurable, and global notion of...
A Polyadic Modal µ-Calculus (1997)
A Polyadic, Danmarks Tekniske Universitet, Henrik Reif Andersen
The propositional ¯-calculus of Kozen extends modal logic with fixed points to achieve a powerful logic for expressing temporal properties of systems modelled by labelled transition systems. We...
On Model Checking Infinite-State Systems (1997)
This paper presents a proof method for proving that infinite-state systems satisfy properties expressed in the modal ¯-calculus. The method is sound and complete relative to externally proving...
Complete Axiomatization of Observation Congruence for PMC (1997)
For Pmc, Danmarks Tekniske Universitet, Henrik Reif Andersen, Michael Mendler
In [AM93b] an asynchronous process algebra with multiple clocks, called PMC, was introduced and a complete axiomatization of strong bisimulation equivalence was given for a class of finite state...
Describing a Signal Analyzer in the Process Algebra PMC - A Case Study (1997)
Henrik Reif Andersen, Michael Mendler
. In this paper we take a look at real-time systems from an implementation-oriented perspective. We are interested in the formal description of genuinely distributed systems whose correct functional...
An Asynchronous Process Algebra with Multiple Clocks (1997)
Henrik Reif Andersen, Michael Mendler
. In this paper we introduce a novel approach to the specification of real-time behaviour with process algebras. In contrast to the usual pattern, involving a fixed, measurable, and global notion of...
An Asynchronous Process Algebra with Multiple Clocks (1997)
Henrik Reif Andersen, Michael Mendler
. In this paper we introduce a novel approach to the specification of real-time behaviour with process algebras. In contrast to the usual pattern, involving a fixed, measurable, and global notion of...
A Process Algebra with Multiple Clocks (1997)
Henrik Reif Andersen, Michael Mendler, Danmarks Tekniske Hjskole
In this report we propose a novel approach to the specification of real-time behaviour based on process algebras. In contrast to the usual pattern, involving a fixed, measurable, and global notion of...
For Pmc, Danmarks Tekniske Universitet, Henrik Reif Andersen, Michael Mendler
In [AM93b] an asynchronous process algebra with multiple clocks, called PMC, was introduced and a complete axiomatization of strong bisimulation equivalence was given for a class of finite state...
Describing a Signal Analyzer in the Process Algebra PMC -- A Case Study (1997)
Henrik Reif Andersen, Michael Mendler
. In this paper we take a look at real-time systems from an implementation-oriented perspective. We are interested in the formal description of genuinely distributed systems whose correct functional...
A Compositional Proof System for the Modal (1997)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal - calculus. The proof system is compositional in the structure...
A Polyadic, Danmarks Tekniske Universitet, Henrik Reif Andersen
The propositional -calculus of Kozen extends modal logic with fixed points to achieve a powerful logic for expressing temporal properties of systems modelled by labelled transition systems. We...
On Model Checking Infinite-State Systems (1997)
This paper presents a proof method for proving that infinite-state systems satisfy properties expressed in the modal -calculus. The method is sound and complete relative to externally proving...
Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion (1997)
. This paper presents an algorithm for solving Boolean fixedpoint equations containing one level of nesting of minimum and maximum fixed points. The algorithm assumes that the equations of the inner...
MuDiv: A Tool for Partial Model Checking (1997)
Henrik Reif Andersen, Jrn Lind-nielsen
MuDiv is a tool for verifying concurrent systems. It is based on the technique of partial model checking described in [1]. The technique uses a variation of the modal -calculus, known as modal...
A Compositional Proof System for the Modal µ-Calculus (1995)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel, Dr. Henrik, Reif Andersen
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal -calculus. The proof system is compositional in the structure...
PMC: A Process Algebra for Real-Time Systems (1995)
Henrik Reif Andersen, Michael Mendler
Most timed process algebras view a real-time system as operating under the regime of a global time parameter constraining the occurrence of actions. By the use of quantitative timing constraints they...
PMC: A Process Algebra for Real-Time Systems (1995)
Henrik Reif Andersen, Michael Mendler
Most timed process algebras view a real-time system as operating under the regime of a global time parameter constraining the occurrence of actions. By the use of quantitative timing constraints they...
A Compositional Proof System for the Modal (1994)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal - calculus. The proof system is compositional in the structure...
Stepwise CTL Model Checking of State/Event Systems (1970)
In this paper we present an efficient technique for symbolic model checking of any CTL formula with respect to a state/event system. Such a system is a concurrent version of a Mealy machine and is...