Fundamenta Informaticae - Volume 85, issue 1-4

Authors: Jüngel, Matthias | Mellmann, Heinrich

Article Type: Research Article

Abstract: In this paper we introduce a state-estimation method that uses a short-term memory to calculate the current state. A common way to solve state estimation problems is to use implementations of the Bayesian algorithmlike Kalman filters or particle filters. When implementing a Bayesian filter several problems can arise. One difficulty is to obtain error models for the sensors and for the state transitions. The other difficulty is to find an adequate compromise between the accuracy of …the belief probability distribution and the computational costs that are needed to update it. In this paper we show how a short-term memory of perceptions and actions can be used to calculate the state. In contrast to the Bayesian filter, this method does not need an internal representation of the state which is updated by the sensor and motion information. It is shown that this is especially useful when information of sparse sensors (sensors with non-uniquemeasurements with respect of the state) has to be integrated. Show more

Keywords: State Estimation, Localization

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 297-311, 2008

Authors: Kacprzak, Magdalena | Nabiałek, Wojciech | Niewiadomski, Artur | Penczek, Wojciech | Półrola, Agata | Szreter, Maciej | Woźna, Bożena | Zbrzezny, Andrzej

Article Type: Research Article

Abstract: The papers presents the current stage of the development of VerICS - a model checker for real-time and multi-agent systems. Depending on the type of a system considered, it enables to test various classes of properties - from reachability to temporal, epistemic and deontic formulas. The model checking methods used to this aim include both SAT-based and enumerative ones. In the paper we focus on new features of the verifier: SAT-based model checking for multi-agent systems …and several extensions and improvements to real-time systems' verification. Show more

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 313-328, 2008

Authors: Köhler-Bußmeier, Michael | Kudlek, Manfred

Article Type: Research Article

Abstract: In this contribution we study an extension of zero-safe nets that allows to model cooperation scenarios. Since zero-safe nets cannot be represented as finite nets in general, we study an extension of the firing rule having a close connection to blind counter automatons and the theory of semi-flows. As a main result we obtain, that a representation can always be given as a finite P/T net – although our firing rule is an extension of the …original one – i.e. it preserves all the events that have been allowed before. Show more

Keywords: debit tokens, semi-flows, zero-safe nets

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 329-342, 2008

Authors: Langmaack, Hans | Salwicki, Andrzej | Warpechowski, Marek

Article Type: Research Article

Abstract: In an earlier article [5] we analyzed the problem of determining direct superclasses in Java and Java-like languages. We gave a specification of the problem showing that it closely reflects the requirements of [2]. We presented a non-deterministic algorithm and proved its correctness and completeness. This paper presents a deterministic algorithm which elaborates direct superclasses. The new algorithm is better for it presents all details of implementation and its cost seems lower than the cost of …the non-deterministic algorithm. Another advantage of the proposed algorithm is error recovery. Should the algorithm report an error it continues its job and possibly reports more errors in one pass. Show more

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 343-357, 2008

Authors: Lomuscio, Alessio | Penczek, Wojciech

Article Type: Research Article

Abstract: We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give the syntax and semantics of a temporal-epistemic securityspecialised logic and provide a lazy-intruder model for the protocol rules that we argue to be particularly suitable for verification purposes. We exemplify the technique by finding a (known) bug in the traditional NSPK protocol.

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 359-375, 2008

Authors: Middelkoop, Ronald | Huizing, Cornelis | Kuiper, Ruurd | Luit, Erik J.

Article Type: Research Article

Abstract: The layering that is present in many OO designs is not accounted for in current interpretations of invariants. We propose to make layers explicit in specifications and introduce a new interpretation of invariants that exploits these layers. Furthermore, we present a sound, modular technique to statically verify that programs satisfy the new interpretation.

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 377-398, 2008

Authors: Mikulski, Łukasz

Article Type: Research Article

Abstract: The behavior of infinite traces is an interesting field for studies. Infinite traces can be described using projections to word monoids. Such projection representations can be generalized to projection sets. To complete simple descriptions, the binary operation from projection sets to traces has been defined. After such preparations some properties of infinite traces are discussed.

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 399-408, 2008

Authors: Nabiałek, Wojciech | Janowska, Agata | Janowski, Paweł

Article Type: Research Article

Abstract: The aim of the work is twofold. In order to face the problem of modeling time constraints in Promela, a timed extension of the language is presented. Next, timed Promela is translated to timed automata with discrete data, that is timed automata extended with integer variables. The translation enables verification of Promela specifications via tools accepting timed automata as input, such as VerICS or Uppaal. The translation is illustrated with a well known example of Fischer's …mutual exclusion protocol. Some experimental results are also presented. Show more

Keywords: Promela, Spin, Timed Automata, timed systems, model checking

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 409-424, 2008

Authors: Penczek, Wojciech | Szreter, Maciej

Article Type: Research Article

Abstract: We present an improvement to the SAT-based Unbounded Model Checking (UMC, for short) algorithm [13]. Our idea consists in building blocking clauses of literals corresponding not only to propositional variables encoding states, but also to more general subformulas over these variables encoding sets of states. This way our approach alleviates an exponential blow-up in the number of blocking clauses. A hybrid algorithm for verifying Timed Automata is proposed, where the timed part of blocking clauses is …computed using Difference Bound Matrices. The optimization results in a considerable reduction in the size and the number of generated blocking clauses, thus improving the overall performance. This is shown on the standard benchmark of Fischer's Mutual Exclusion protocol. Show more

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 425-440, 2008

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: Parsing Expression Grammar (PEG) is a new way to specify syntax, by means of a topdown processwith limited backtracking. It can be directly transcribed into a recursive-descent parser. The parser does not require a separate lexer, and backtracking removes the usual LL(1) constraint. This is convenient for many applications, but there are two problems: PEG is not well understood as a language specification tool, and backtracking may result in exponential processing time. The paper consists of …two parts that address these problems. The first part is an attempt to find out the language actually defined by a given parsing expression. The second part reports measurements of backtracking activity in a PEG-derived parser for the programming language C. Show more

Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 441-451, 2008