[All BiBTeX entries for this year]

B.C.M. Wondergem, P. van Bommel, and Th.P. van der Weide. * Counting and Generating (Boolean) Index Expressions. *Technical report, University of Nijmegen, 1999, Technical Report CSI-R99xx.

[ Missing PDF ] [ Bibtex ]

A.T. Arampatzis, Th.P. van der Weide, C.H.A. Koster, and P. van Bommel. * Text Filtering using Linguistically-motivated Indexing Terms. *Technical report: CSI-R9901, January, Computing Science Institute, University of Nijmegen, Nijmegen, The Netherlands, EU, 1999.

In this article we describe a number of text filtering experiments based on indexing terms other than simple keywords. These experiments were conducted as a first step of validating a phrase-based retrieval model. Our approach in the selection of indexing terms was based on a part-of-speech tagger and shallow parsing. Different types of indexing terms were evaluated, including keywords, nouns, verbs, adverbs, adjectives, adjacent word-pairs and head-modifier pairs. Furthermore, the effect of lemmatizing terms was investigated. Evaluation was done with three utility-based measures and average set precision. We managed to obtain experimental evidence that the phrase-based retrieval model performs better than keyword-based models. Our experiments showed that an indexing set of keywords can be reduced by retaining only some certain part-of-speech categories without any substantial negative impact in performance; in some cases the effectiveness even improved. Furthermore, we found that lemmatization can produce confusion between nouns and verbs decreasing effectiveness, while overall it is beneficial especially for phrasal terms.

**Keywords:**
Text-Filtering, Natural Language Processing, Indexing, Rocchio, Binary Terms, Lemmatization.

P.A. Jones, P. van Bommel, C.H.A. Koster, and Th.P. van der Weide. * Best First Search techniques in Document Processing applications. *Technical report: CSI-R9902, January, Radboud University Nijmegen, 1999.

[ Missing PDF ] [ Bibtex ]

M.C.A. Devillers. * Translating IOA automata to PVS. *Technical report: CSI-R9903, February, Radboud University Nijmegen, 1999.

IOA is a specification language for input/output automata based on the model of Lynch and Tuttle; IOA is developed at MIT by Garland and Lynch and is a part of the Larch family of specification languages. We present a compiler which translates IOA specifications to input for the Prototype Verification System (PVS) by means of examples.

[ Missing PDF ] [ Bibtex ]

M.I.A. Stoelinga. * Gambling for Leadership: Verification of Root Contention in IEEE 1394. *Technical report: CSI-R9904, March, Radboud University Nijmegen, 1999.

[ Missing PDF ] [ Bibtex ]

M.I.A. Stoelinga, and F.W. Vaandrager. * Root Contention in IEEE 1394. *Technical report: CSI-R9905, March, Radboud University Nijmegen, 1999.

The model of probabilistic I/O automata of Segala and Lynch is used for the formal specification and analysis of the root contention protocol from the physical layer of the IEEE 1394 (""FireWire"") standard. In our model of the protocol both randomization and real-time play an essential role. In order to make our verification easier to understand we introduce several intermediate automata in between the implementation and the specification automaton. This allows us to use very simple notions of refinement rather than the more general but also very complex simulation relations which have been proposed by Segala and Lynch.

B.P.F. Jacobs. * The Temporal Logic of Coalgebras via Galois Algebras. *Technical report: CSI-R9906, April, Radboud University Nijmegen, 1999.

This paper introduces a temporal logic for coalgebras.Nexttime and lasttime operators are defined for a coalgebra,acting on predicates on the state space. They give rise towhat is called a Galois algebra.Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebrasturns out to be functorial, yielding indexed categorical structures. This gives many examples, for coalgebras ofpolynomial functors on sets. Additionally, it will be shown how``fuzzy'' predicates on metric spaces, and predicates onpresheaves, yield indexed Galois algebras, in basically thesame coalgebraic manner.

[ Missing PDF ] [ Bibtex ]

N. Lynch, R. Segala, F.W. Vaandrager, and H.B. Weinberg. * Hybrid I/O Automata. *Technical report: CSI-R9907, April, Radboud University Nijmegen, 1999.

We propose a new hybrid automaton model that is capable ofdescribing both continuous and discrete behavior.The model, which extends the timed automaton model of Lynch & Vaandrager, and the phase transition system models of Maler, Manna & Pnueli, and of Alur et al, allows communication among components using both sharedvariables and shared actions.The main contributions of this paper are:(1) a definition of hybrid automata and of an implementationrelation based on hybrid traces,(2) a definition of a simulation between hybrid automata anda proof that existence of a simulation implies the implementation relation,(3) a definition of composition and hiding operations on hybridautomata and a proof that these operations respect the implementation relation,(4) a definition of hybrid I/O automata, which specialize hybridautomata by an additional distinction between input and output, and a proof that the results on simulation relations, composition and hiding carry over to this new setting, and(5) a definition of receptiveness for hybrid I/O automata anda proof that, assuming certain compatibility conditions, receptiveness is preserved by composition.

A. Fehnker. * Scheduling a steel plant with timed automata. *Technical report: CSI-R9910, July, Radboud University Nijmegen, 1999.

Scheduling in an environment with a large number of constraints is known to be a hard problem. We tackle this problem for a integrated steel plant in Ghent, Belgium, using Uppaal, a model checker for networks of timed automata. We show how to translate schedulability to reachability,enabling us to use Uppaals model checking algorithms.

B.C.M. Wondergem, P. van Bommel, and Th.P. van der Weide. * Compactness of Boolean Index Expressions. *Technical report: CSI-R9911, June, Radboud University Nijmegen, 1999.

Boolean index expressions (BIEs) form an expressive and tractable descriptor language for text representation. Another advantage is that BIEs are compact, meaning that equivalent Boolean combinations of (regular) index epressions require more terms, connectors, and logical operators. In this article, it is investigated how compact BIEs are. Two classes od BIEs are defined that illustrate the bounds on the compactness of BIEs: minimal and maximal BIEs. The bounds are explicitly derived and illustrated by generic examples.

[ Missing PDF ] [ Bibtex ]

M. Huisman, and B.P.F. Jacobs. * Java Program Verification via a Hoare Logic with Abrupt Termination. *Technical report: CSI-R9912, June, Radboud University Nijmegen, 1999.

This paper formalises a semantics for statements andexpressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, return orcontinue). This extends the traditional semantics underlying e.g. Hoare logic, which only distinguishes termination and non-termination. An extension of Hoare logic is elaborated that includes means for reasoning about abrupt termination (and side-effects). It prominently involves rules for reasoning about while loops, which may contain exceptions, breaks, continues and returns. This extension applies in particular to Java. As an example, a standard pattern search algorithm in Java (involving a while loop with returns) is proven correct using the proof-tool PVS.

[ Missing PDF ] [ Bibtex ]

M.J. de Mol, and M.C.J.D. van Eekelen. * A Prototype Dedicated Theorem Prover for Clean. *Technical report: CSI-R9913, October, Radboud University Nijmegen, 1999.

This paper examines an approach to computer assisted formal reasoning in relation to functional programming. Instead of using a generic proof tool which may differ on some points from the functional language used, a new proof tool is to bedeveloped which is solely intended for proving properties of programs written in one specific language. This proof tool is intended to be inserted in the Integrated Development Environment of the programming language, which ensures a seamless integration. A prototype approximating such a proof tool for the pure, lazy functional programming language Clean has been implemented and will be described in this paper. It will be shown how this prototype can be used and examples of theorems that can be proven with it will be given. An examination will be made of the work that needs to be done to extend the prototype to an integrated programming tool.

H. Wupper. * Anatomy of Computer Systems - Experiences with a new introductory informatics course. *Technical report: CSI-R9914, August, Radboud University Nijmegen, 1999.

S. Ivanov, and W.O.D. Griffioen. * Verification of a Biphase Mark Protocol. *Technical report: CSI-R9915, August, Radboud University Nijmegen, 1999.

We show how a symbolic model checker for linear hybridautomata can be used to analyze a biphase mark protocol.This protocol was first verified formally by Moore using a model of asynchrony.In this paper we demonstrate that algorithmic methods can automatically verify the correctness of the protocol for wider clock drifts.Unlike Moore, our model allows for clock jitter.We believe that linear hybrid automata enable a natural way ofmodeling the protocol.

I. Bethke, J.W. Klop, and R. de Vrijer. * Extending Partial Combinatory Algebras. *Technical report: CSI-R9920, October, Radboud University Nijmegen, 1999.

We give a negative answer to the question whether every partial combinatory algebra can be completed. The explicit counterexample will be an intricately constructed term model, the construction and the proof that it works heavily depending on syntactic techniques. In particular, it is a nice example of reasoning with elementary diagrams and descendants. We also include a domain-theoric proof of the existence of an incompletable partial combinatory algebra.

I. Bethke, J.W. Klop, and R. de Vrijer. * Descendants and Origins in Term Rewriting. *Technical report: CSI-R9921, October, Radboud University Nijmegen, 1999.

In this paper we treat various aspects of a notion that is central in term rewriting, namely that of descendants or residuals. We address both first order term rewriting and l-calculus, their finitary as well as their infinitary variants. A recurrent theme is the Parallel Moves Lemma. Next to the classical notion of descendant, we introduce an extended version, known as �origin tracking�. Origin tracking has many applications. Here it is employed to give new proofs of three classical theorems: the Genericity Lemma in l-calculus, the theorem of Huet and L�vy on needed reductions in first order term rewriting, and Berry�s Sequentiality Theorem in (infinitary) l-calculus.Note: This article is based on a lecture given by Jan Willem Klop at RTA�98 held in Tsukuba, Japan.

J.J. Sarbo, and J.I. Farkas. * Sign Grammar. *Technical report: CSI-R9922, October, Radboud University Nijmegen, 1999.

Sign Grammar is a dependency based approach to syntactic structure in which the dependency relations are derived on a semiotic basis, from C.S. Peirce�s theory of s igns. We illustrate the potential of Sign Grammar by using English as an example. We argue that, by means of its syntactic structures, the English language implements signs analogous to �real� world signs introduced by C.S. Peirce. No familiarity with semiotic is assumed in the paper.

P. Lambooij. * The YAPI protocol for buffered data transfer. *Technical report: CSI-R9923, December, Radboud University Nijmegen, 1999.

A case study is presented of tool-assisant verification of a protocol used in industry to model Kahn processing networks. The object oriented specification language CCSL is used to describe the point to point communication between nodes in the network. CCSL is translated into the mathematical theories of coalgebras via a special compiler. These theories form the basis of a rigorous proof of correctness of data transfer and absence of deadlock in the protocol. Proofs are developed using the PVS system.

J.A.G.M. van den Berg, M. Huisman, B.P.F. Jacobs, and E. Poll. * A Type-Theoretic Memory Model for Verification of Sequential Java Programs. *Technical report: CSI-R9924, November, Radboud University Nijmegen, 1999.

This paper explains the details of the memory model underlying the verification of sequential Java programs in the framework of the �LOOP project. The building blocks of this memory are cells, which are untyped in the sense that they can store the contents of the fields of an arbitrary Java object. The main memory is then modeled as three infinite series of such cells, for storing instance variables on a heap, local variables and parameters on a stack, and static (or class)variables in the third series. Verification on the basis of this memory model is illustrated both in PVS and in Isabelle/HOL, via several examples of Java programs, involving various subtleties of the language (wrt. memory storage).

H.X. Willems. * Compact Timed Automata for PLC Programs. *Technical report: CSI-R9925, December, Radboud University Nijmegen, 1999.

In this work a set of tools is developed to convert programsfor Programmable Logic Controllers (PLCs) into timed automata in order to facilitate the verification of such programs.It is shown that our timed automaton models of PLC programscan be dissected into a timed and an untimed part. Typically, the untimed part is much larger than the timed partand can be reduced in size by using the CADP toolset.The reduction in state space is substantial, even for smallPLC programs.

B.P.F. Jacobs, and E. Poll. * A Monad for Basic Java Semantics. *Technical report: CSI-R9926, December, Radboud University Nijmegen, 1999.

This paper describes the role of a computational monad in the denotational semantics of sequential Java and investigates some of its properties. This denotational semantics is an abstraction of the one used for the verification of (sequential) Java programs using proof tools, see [8,12].

E. Poll. * The Type System of Aldor. *Technical report: CSI-R9928, December, Radboud University Nijmegen, 1999.

This paper gives a formal description of (at least a part of) the type system of Aldor, the extension language of the computer algebra system AXIOM. In the process of doing this a critique of the design of the system emerges.