@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@TechReport{BRICS-DS-98-3,
author = "Sunesen, Kim",
title = "Reasoning about Reactive Systems",
institution = brics,
year = 1998,
type = ds,
number = "DS-98-3",
address = daimi,
month = dec,
note = "PhD thesis. xvi+204~pp",
abstract = "The main concern of this thesis is the formal reasoning
about reactive systems.\bibpar
We first consider the automated verification of safety
properties of finite systems. We propose a practical
framework for integrating the behavioural reasoning about
distributed reactive systems with model-checking methods.
We devise a small self-contained theory of distributed
reactive systems including standard concepts like
implementation, abstraction, and proof methods for
compositional reasoning. The proof methods are based on
trace abstractions that relate the behaviours of the
program with the specification. We show that trace
abstractions and the proof methods can be expressed in a
decidable Monadic Second-Order Logic (M2L) on words. To
demonstrate the practical pertinence of the approach, we
give a self-contained, introductory account of the method
applied to an RPC-memory specification problem proposed
by Broy and Lamport. The purely behavioural descriptions
which we formulate from the informal specifications are
written in the high-level symbolic language FIDO, a
syntactic extension of M2L. Our solution involves
FIDO-formulas more than 10 pages long. They are
translated into M2L-formulas of length more than 100
pages which are decided automatically within minutes.
Hence, our work shows that complex behaviours of reactive
systems can be formulated and reasoned about without
explicit state-based programming, and moreover that
temporal properties can be stated succinctly while
enjoying automated analysis and verification.\bibpar
Next, we consider the theoretical borderline of
decidability of behavioural equivalences for
infinite-state systems. We provide a systematic study of
the decidability of non-interleaving linear-time
behavioural equivalences for infinite-state systems
defined by CCS and TCSP style process description
languages. We compare standard language equivalence with
two generalisations based on the predominant approaches
for capturing non-interleaving behaviour: pomsets
representing global causal dependency, and locality
representing spatial distribution of events. Beginning
with the process calculus of Basic Parallel Processes
(BPP) obtained as a minimal concurrent extension of
finite processes, we systematically investigate
extensions towards full CCS and TCSP. Our results show
that whether a non-interleaving equivalence is based on
global causal dependency between events or whether it is
based on spatial distribution of events can have an
impact on decidability. Furthermore, we investigate
tau-forgetting versions of the two non-interleaving
equivalences, and show that for BPP they are
decidable.\bibpar
Finally, we address the issue of synthesising distributed
systems -- modelled as elementary net systems -- from
purely sequential behaviours represented by
synchronisation trees. Based on the notion of regions,
Ehrenfeucht and Rozenberg have characterised the
transition systems that correspond to the behaviour of
elementary net systems. Building upon their results, we
characterise the synchronisation trees that correspond to
the behaviour of active elementary net systems, that is,
those in which each condition can always cease to hold.
The identified class of synchronisation trees is
definable in a monadic second order logic over infinite
trees. Hence, our work provides a theoretical foundation
for smoothly combining techniques for the synthesis of
nets from transition systems with the synthesis of
synchronisation trees from logical specifications",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@TechReport{BRICS-DS-98-2,
author = "Lassen, S{\o}ren B.",
OPTauthor = "Lassen, S{\o}ren B{\o}gh",
title = "Relational Reasoning about Functions and Nondeterminism",
institution = brics,
year = 1998,
type = ds,
number = "DS-98-2",
address = daimi,
month = dec,
note = "PhD thesis. x+126~pp",
abstract = "This dissertation explores a uniform, relational proof
style for operational arguments about program
equivalences. It improves and facilitates many
previously given proofs, and it is used to establish new
proof rules for reasoning about term contexts, recursion,
and nondeterminism in higher-order programming
languages.\bibpar
Part I develops an algebra of relations on terms and
exploits these relations in operational arguments about
contextual equivalence for a typed deterministic
functional language. Novel proofs of the basic laws,
sequentiality and continuity properties, induction rules,
and the CIU Theorem are presented together with new
relational proof rules akin to Sangiorgi's ``bisimulation
up to context'' for process calculi.\bibpar
Part II extends the results from the first part to
nondeterministic functional programs. May and must
operational semantics and contextual equivalences are
defined and their properties are explored by means of
relational techniques. For must contextual equivalence,
the failure of ordinary syntactic $\omega$-continuity in
the presence of countable nondeterminism is addressed by
a novel transfinite syntactic continuity principle. The
relational techniques are also applied to the study of
lower and upper applicative simulation relations,
yielding new results about their properties in the
presence of countable and fair nondeterminism, and about
their relationship with the contextual equivalences",
linkhtmlabs = "",
OPTcomment = "",
OPTlinkdvi = "",
linkps = "",
linkpdf = ""
}
@TechReport{BRICS-DS-98-1,
author = "Hougaard, Ole I.",
OPTauthor = "Ole Ildsgaard Hougaard",
title = "The {CLP(OIH)} Language",
institution = brics,
year = 1998,
type = ds,
number = "DS-98-1",
address = daimi,
month = feb,
note = "PhD thesis. xii+187~pp",
abstract = "Many type inference problems are different instances of
the same constraint satisfaction problem. That is, there
is a class of constraints so that these type inference
problems can be reduced to the problem of finding a
solution to a set of constraints. Furthermore, there is
an efficient constraint solving algorithm which can find
this solution in polynomial time.\bibpar
We have shown this by defining the appropriate constraint
domain, devising an efficient constraint satisfaction
algorithm, and designing a constraint logic programming
language over the constraint domain. We have implemented
an interpreter for the language and have thus produced a
tool which is well-suited for type inference problems of
different kinds.\bibpar
Among the problems that can be reduced to our constraint
domain are the following:
\begin{itemize}
\item The simply typed $\lambda$-calculus.
\item The $\lambda$-calculus with subtyping.
\item Arbadi and Cardelli's Object calculus.
\item Effect systems for control flow analysis.
\item {\sf Turbo Pascal}.
\end{itemize}
With the added power of the constraint logic programming
language, certain type systems with no known efficient
algorithm can also be implemented --- e.g.\ the object
calculus with {\sf selftype}.\bibpar
The programming language thus provides a very easy way of
implementing a vast array of different type inference
problems",
linkhtmlabs = "",
OPTcomment = "",
OPTlinkdvi = "",
linkps = "",
linkpdf = ""
}