[All BiBTeX entries for this year]

R.D.T. Janssen, and H.A. (Erik) Proper. * A functionality taxonomy for document search engines. *Technical report, June, Ordina Institute, Gouda, The Netherlands, EU, 2001.

In this paper a functionality taxonomy for document search engines is proposed. It can be used to assess the features of a search engine, to position search engines relative to each other, or to select which search engine `fits' a certain situation. One is able to identify areas for improvement. During development, we were guided by the viewpoint of the user. We use the word `search engine' in the broadest sense possible, including library and web based (meta) search engines.

The taxonomy distinguishes seven functionality areas: an indexing service, user profiling, query composition, query execution, result presentation, result refinement, and history keeping. Each of these relates and provides services to other functionality areas. It can be extended whenever necessary.

To illustrate the validity of our taxonomy, it has been used for comparing various document search engines existing today (ACM Digital Library, PiCarta, Copernic, AltaVista, Google, and GuideBeam). It appears that the functionality aspects covered by our taxonomy can be used for describing these search engines.

E. Poll, and J. Zwanenburg. * From Algebras and Coalgebras to Dialgebras. *Technical report: CSI-R0101, January, Radboud University Nijmegen, 2001.

This paper investigates the notion of dialgebra, which generalises the notions of algebra and coalgebra. We show that many (co)algebraic notions and results can be generalised to dialgebras, and investigate the essential differences between (co)algebras and arbitrary dialgebras.

[ Missing PDF ] [ Bibtex ]

T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager. * Linear Parametric Model Checking of Timed Automata. *Technical report: CSI-R0102, January, Radboud University Nijmegen, 2001.

We present an extension of the model checker Uppaal, capable of synthesizing linear parameter constraints for the correctness of parametric timed automata. The symbolic representation of the (parametric) state-space is shown to be correct. A second contribution of this paper is the identification of a subclass of parametric timed automata (L/U automata), for which the emptiness problem isdecidable, contrary to the full class where it is know tobe undecidable. Also, we present a number of lemmas enabling the verification effort to be reduced for L/U automata in some cases. We illustrate our approach by deriving linear parameter constraints for a number of well-known case studies from the literature (exhibiting a flaw in a published paper).

A.T. Arampatzis, J. Beney, C.H.A. Koster, and Th.P. van der Weide. * KUN on the TREC-9 Filtering Track: Incrementality, Decay, and Threshold Optimization for Adaptive Filtering Systems. *Technical report: CSI-R0104, January, Radboud University Nijmegen, 2001.

[ Missing PDF ] [ Bibtex ]

M.I.A. Stoelinga. * Fun with FireWire: Experiences with Verifying the IEEE 1394 Root Contention Protocol. *Technical report: CSI-R0107, March, Radboud University Nijmegen, 2001.

The IEEE 1394 Root Contention Protocol is leader election algorithm for two processes and has been analysed in various case studies. This paper compares several formal verification techniques applied to this protocol.

[ Missing PDF ] [ Bibtex ]

M. Hendriks. * Translating Uppaal to Not Quite C. *Technical report: CSI-R0108, March, Radboud University Nijmegen, 2001.

This project presents a simple translation from Uppaal models of real-time controllers to NQC programs. The modeling of these controllers in Uppaal provides a way to verify the requirements on these controllers. The user directs the translation by defining a type for each variable used in the model and by assigning each automaton in the model to a controller.The translation, that has been implemented in the tool uppaal2nqc, results in a set of NQC programs that, when all NQC programs are run concurrently, approximately realizes a subset of the executions of the model.An Uppaal model of controllers of an experimental LEGO setup has been translated and the resulting NQC programs have been run in this setup to validate the translation.

[ Missing PDF ] [ Bibtex ]

G. Behrmann, A. Fehnker, T.S. Hune, K.G. Larsen, P. Pettersson, J.M.T. Romijn, and F.W. Vaandrager. * Minimum-Cost Reachability for Priced Timed Automata. *Technical report: CSI-R0109, March, Radboud University Nijmegen, 2001.

This paper introduces the model of linearly priced timed au-tomata as an extension of timed automata, with prices on both transitions and locations. For this model we consider the minimum-cost reachability problem: i.e. given a linearly priced timed automaton and a target state, determine the minimum cost of executions from the initial state to the target state. This problem generalizes the minimum-time reachability problem for ordinary timed automata. We prove decidability of this problem by offering an algorithmic solution, which is based on a combination of branch-and-bound techniques and a new notion of pricedregions. The latter allows symbolic representation and manipulation of reachable states together with the cost of reaching them.

G. Behrmann, A. Fehnker, T.S. Hune, K.G. Larsen, P. Pettersson, and J.M.T. Romijn. * Efficient Guiding Towards Cost-Optimality in UPPAAL. *Technical report: CSI-R0110, March, Radboud University Nijmegen, 2001.

In this paper we present an algorithm for efficiently computing the minimum cost of reaching a goal state in the model of Uniformly Priced Timed Automata (UPTA). This model can be seen as a submodel of the recently suggested model of linearly priced timed automata, whichextends timed automata with prices on both locations and transitions. The presented algorithm is based on a symbolic semantics of UTPA, and an efficient representation and operations based on difference bound matrices. In analogy with Dijkstra's shortest path algorithm, we show that the search order of the algorithm can be chosen such that the number of symbolic states explored by the algorithm is optimal, in the sense that the number of explored states can not be reduced by any other search order based on the cost of states. We also present a number of techniquesinspired by branch-and-bound algorithms which can be used for limiting the search space and for quickly finding near-optimal solutions.The algorithm has been implemented in the verification tool Uppaal. When applied on a number of experiments the presented techniques reduced the explored state-space with up to 90%.

[ Missing PDF ] [ Bibtex ]

R. Gieben. * Chain of Trust. *Technical report: CSI-R0111, March, Radboud University Nijmegen, 2001.

DNSSEC is the intended successor of DNS (Domain Name System), the well-known system that takes care of the mapping between domain names and IP numbers on the internet. There are however some security problems with DNS, thus the need for DNSSEC (DNS SECure). DNSSEC uses public key cryptography to solve the security issues in the DNS. The goal of DNSSEC is to create a chain of trust in which a top level zone (like com) signs the key of a lower zone (such as child.com) which in turn can sign a even lower zone (a.child.com, for instance). To set up this chain, keys must be exchanged and signatures must be renewed on a regular basis. Furher more, keys can be discoverd, lost or stolen. This master thesis delves into those problems and presents possible solutions and procedures for efficient and (reasonably) safe distribution and renewal of keys and signatures.

[ Missing PDF ] [ Bibtex ]

A.H. Mader, E. Brinksma, H. Wupper, and N. Bauer. * Design of a PLC Control Program for a Batch Plant VHS Case Study 1. *Technical report: CSI-R0113, March, Radboud University Nijmegen, 2001.

[ Missing PDF ] [ Bibtex ]

U. Hannemann, and J.J.M. Hooman. * Top-down Design of a Command-and-Control System with Timing Assumptions . *Technical report: CSI-R0116, June, Radboud University Nijmegen, 2001.

We present a formal approach to the top-down design ofreal-time components that communicate using a shared data space. The approach is compositional, that is, only the formal specifications of the components are used toreason about their combined behaviour. Formal reasoning is supported by the interactive theorem prover PVS.Our shared data space model is based on the softwarearchitecture SPLICE, that allows loosely-coupled components. Our formalism is illustrated by the top-down design of a small flight-tracking-and-display system, whichcontains an event-driven and a time-driven component.Formal correctness is established, given suitableassumptions about the environment of the system andrelations between timing parameters.

J.J. Sarbo, and J.I. Farkas. * On the isomorphism of sign, logic and language. *Technical report: CSI-R0117, June, Radboud University Nijmegen, 2001.

Formal models of natural language often suffer from their excessive complexity which, in our opinion, may be due to the underlying approach itself. In this paper we introduce a semiotic model of language which is only linearly complex.The existence of such a model is conform with the experience that language is a real-time complex phenomenon.

[ Missing PDF ] [ Bibtex ]

F.A. Grootjen. * Relational indexing using a grammarless parser. *Technical report: CSI-R0118, July, Radboud University Nijmegen, 2001.

This article proposes an altenate view on natural language parsing. Instead of looking for some predifined (phrase) structure it takes inter-word relations as startingpoint. The reason for this is twofold: firstly it circumvents traditional parsing and linguistic problems and secondly it offers a possibility to extract information specifically needed by IR applications. The close relationship with index expressions opens the door to feedback mechanisms like 'Query By Navigation"" [Bruza and van der Weide, 1992] and conceptual knowledge extraction [Grootjen, 2000]. The presented ideas are accompanied by an implementation and a small scale experiment.

[ Missing PDF ] [ Bibtex ]

J.I. Farkas, and J.J. Sarbo. * A Peircean Ontology of Semantics. *Technical report: CSI-R0120, Nijmegen Institute for Information and Computing Sciences, University of Nijmegen, Nijmegen, The Netherlands, EU, 2001.

Peirce's semiotics can be effectively used for modeling different types of signs. In this paper it is argued that semantic signs, which are signs from the semantic point of view, are no exception. It turns out, however, that a proper modeling of semantic signs needs a better understanding of the concept of qualisigns, as well as, of the relation between Peirce's categories and his theory of signs.

[ Missing PDF ] [ Bibtex ]

J.J. Sarbo, and J.I. Farkas. * A linearly complex model for knowledge representation. *Technical report: CSI-R0121, Nijmegen Institute for Information and Computing Sciences, University of Nijmegen, Nijmegen, The Netherlands, EU, 2001.

We present two results which complete and extend our Peircean semiotic model of signs introduced earlier. The first result is concerned with the potential of that model for the representation of knowledge in general. The second one formally proves that such a model can be linearly complex.

[ Missing PDF ] [ Bibtex ]

M. Hendriks, and K.G. Larsen. * Exact Acceleration of Real-Time Model Checking. *Technical report: CSI-R0122, December, Radboud University Nijmegen, 2001.

Different time scales do often occur in real-time systems, e.g., a polling real-time system samples the environment many times per second, whereas the environment may only change a few times per second. When these systems are modeled as (networks of) timed automata, the validation using symbolic model checking techniques can significantly be slowed down by unnecessary fragmentation of the symbolic state space.This paper introduces a syntactical adjustment to a subset of timed automata that addresses this fragmentation problem and can speed-up forward symbolic reachability analysis in a significant way. We prove that this syntactical adjustment does not alter reachability properties and that it indeed is effictive. We illustrate our exact acceleration tehnique with run-time date obtained with the model checkers UPPAAL and KRONOS.

[ Missing PDF ] [ Bibtex ]