Academic

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.