I am a graduate student at the Department
of Computer Science at Aalborg University.
Papers and Technical Reports
I have co-authored the following projects during my attendance.
-
Thesis: On-The-Fly Model Checking of Weighted Computation Tree Logic (2013) PDF
We present min-max graphs; a technique to encode the model checking problem of weighted
Computation Tree Logic (CTL), with nonnegative constraints on the modalities, against
weighted Kripke structures.
We outline previous efforts to encode this problem using dependency graphs and their symbolic extension.
We demonstrate how to model check weighted CTL through fixed-point computation on a graph that encodes
the problem, using global and local/on-the-fly fixed-point algorithms.
Moreover, we have implemented the algorithms and evaluated their performance through experiments.
In turn, we conclude that the local approach is often very advantageous.
-
Local Modal Checking of Weighted CTL with Upper-Bound Constraints (2013) PDF
We present a symbolic extension of dependency graphs by
Liu and Smolka in order to model-check weighted Kripke structures
against the logic CTL with upper-bound weight counstraints. Our ex-
tension introduces a new type of edges into dependency graphs and lifts
the computation of fixed-points from boolean domain to nonnegative
integers in order to cope with the weights. We present both global and
local algorithms for the fixed-point computation on symbolic dependency
graphs and argue for the advantages of our approach compared to the
direct encoding of the model checking problem into dependecy graphs.
We implement all algorithms in a publicly available tool prototype and
evaluate them on several experiments. The principal conclusion is that
our local algorithm is the most efficient one with an order of magni-
tute improvement on model checking problems with a high number of
“witnesses”.
-
Local Modal Checking of Weighted CTL (2012) PDF
Local or ”on-the-fly” model checking techniques have be-
come attractive over the years, due to the way they explore the state-
space incrementally, potentially reducing space and time requirements for
analysis and verification. We demonstrate how Liu and Smolkas depen-
dency graph framework and local algorithm for evaluating alternating-
free fixed points can be used to decide satisfaction of weighted CTL
formulae over weighted Kripke structures. This is achieved by encod-
ing the problem as a dependency graph that is pseudo-polynomial in the
size of the bound of the formula. We propose an extension of dependency
graphs called symbolic dependency graphs and a local algorithm for this
framework. We show that the symbolic encoding is polynomial in the
size of the formula and model. Lastly, we demonstrate the advantages of
our approach through experiments.
-
Realizability of Live Sequence Charts (2012) PDF
Live Sequence Charts (LSC) is a graphical formalism for
defining inter-object communication in an intuitive way. Their precise semantics
makes it possible for developers to check for inconsistencies in the specification
of a system, composed of a set of LSCs, and to automatically synthesize a conforming
controller. We propose a syntax and semantics for a subset of LSCs and present a
tool that enables the user to specify system requirements with this subset of the
LSC formalism. The tool is able to determine by means of a game-theoretic approach,
also introduced in this work, whether the specification of a system is realizable.
In this way the tool allows for the specification of a system in an intuitive way
and immediately states whether the design can be implemented or if there are any
contradicting requirements.
-
The Concurrent Real-Time Task Model (2011) PDF
The Digraph Real-time Task model (DRT) was recently in troduced
as a new modeling formalism for uniprocessor schedulability analysis of real-time
systems with sporadic jobs. We extend the syntactical expressiveness of the DRT
model by introducing the Concurrent Real-time Task model (CRT), where parallel constructions
are allowed within tasks. We show how the CRT model can be expressed through a grammar
and then demonstrate how the concept of the demand bound function and utilization
may be adapted to this formalism. Lastly, we argue that the pseudo-polynomial feasibility
results for the DRT model also apply to this model and show how the demand bound
function and utilization may be computed by the means of path abstraction.
-
Bachelor: Petri Nets with Discrete Variables (2011)
PDF
Petri nets are a well-known graphical language for conceptual
modelling. We propose a new model called Petri nets with discrete variables (PNDVs)
that permits additional modelling convenience over classical Petri nets. We show
that PNDVs are Turing complete and give a limited subset with the same expressive
power as Petri nets. Moreover, we demonstrate that PNDVs can simulate bounded discrete
timed-arc Petri nets. We apply heuristic algorithms for reachability analysis of
PNDVs with a tool, we have developed called PeTe. Finally, we demonstrate the advantages
of these algorithms with experimental results from using this tool.
-
Leading Edge Triangulation of Bayesian NWs (2010) PDF
In this report we propose two improvements to reduce the
search space for state-of-the-art optimal triangulation algorithms, with respect
to the total table size criterion. The improvements, we propose, exploit properties
of triangulated graphs and can be applied to any triangulation algorithm, searching
in the space of all elimination orders. This report also covers the basis for inference
in Bayesian networks and introduces the problem of triangulation. We examine heuristics,
minimal and optimal methods for solving this problem. Finally, we compare the methods
discussed and show that it is possible to achieve considerable improvements in the
efficiency of optimal methods.
-
Groo Programming Language (2010) PDF
This report documents the groo programming language. This
includes design decisions, syntax analysis, contextual analysis and execution of
a groo program. A formal operational semantics is given for the groo language as
well as a formal description of the type system. A lexer and parser generator has
been implemented to conduct the syntax analysis, and a type checker to conduct the
contextual analysis. Finally, a recursive interpreter and a virtual machine, which
can be used to execute groo programs, have been implemented.
-
Foodolini - A Food Management System (2009) PDF
This report documents the analysis, design and implementation
of the system Foodolini. Foodolini is designed to administrate food storage in the
private household. This information can then be used for suggesting recipes and
creating a shopping list. This project was conducted using the OOA&D method for
analysis and design of the functionality and class structure, the ADRIA method for
user-interface design and the IDA method for usability evaluation. This report documents
how these methods were applied to create Foodolini, from the analysis where the
functionality was determined, through the design phase and finally the test and
usability evaluation where the final result was evaluated. This report extensively
documents this process with documents, diagrams and pictures.
-
Real-time Ray Tracing (2009) PDF
This report is about real-time ray tracing. Ray tracing
is a technique, which models the way light interacts with surfaces, to create realistic
graphics. We start by investigating how the film and gaming industry make use of
realistic graphics and how current developments may encourage the use of ray tracing
for these applications. The next part of this report covers computer graphics theory,
with an introduction to two rendering techniques called rasterization and ray tracing.
In addition the mathematical foundation of ray tracing is covered. We then move
on to describe lighting, materials, shadows and Monte Carlo ray tracing. In the
following part we implement our own ray tracer, where we discuss the results. Then
we discuss an interview with a senior software developer at Pixar to find out how
the film industry benefits from ray tracing. Finally, we discuss how ray tracing
can be made as fast as possible, so as to make it a real-time rendering solution.
Conferences
© Lars Østergaard 2012