Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Purchase individual online access for 1 year to this journal.
Price: EUR 410.00Impact Factor 2024: 0.4
Fundamenta Informaticae is an international journal publishing original research results in all areas of theoretical computer science. Papers are encouraged contributing:
- solutions by mathematical methods of problems emerging in computer science
- solutions of mathematical problems inspired by computer science.
Topics of interest include (but are not restricted to): theory of computing, complexity theory, algorithms and data structures, computational aspects of combinatorics and graph theory, programming language theory, theoretical aspects of programming languages, computer-aided verification, computer science logic, database theory, logic programming, automated deduction, formal languages and automata theory, concurrency and distributed computing, cryptography and security, theoretical issues in artificial intelligence, machine learning, pattern recognition, algorithmic game theory, bioinformatics and computational biology, quantum computing, probabilistic methods, & algebraic and categorical methods.
Article Type: Research Article
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. i-i, 2008
Authors: Mirkowska, Grażyna | Salwicki, Andrzej | Swida, Oskar
Article Type: Research Article
Abstract: Our aim is to present a methodology that integrates all phases of software¡¯s production beginning from the specification phase, through the phase of programming and finally the phase of verification of program against its specification. The theoretical background of the methodology is algorithmic logic [8]. The environment for practical activities of this software project is a plugin SpecVer [11] extending the Eclipse development platform [2].
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 1-17, 2008
Authors: Bednarczyk, Marek A. | Pawłowski, Wiesław | Bernardinello, Luca | Pomello, Lucia | Borzyszkowski, Tomasz
Article Type: Research Article
Abstract: We are concerned with the problem of defining a complex, hybrid, agent based discrete system in a modular way. Themodularity results from looking at the system from a number of different perspectives, each dealing with a specific aspect of the system. As a solution a synchronization operator is proposed which glues agent aware systems on shared agents and transitions. The construction turns out to be a categorical product. We also show that a logic to talk …about the temporal and the structural properties of the product can be obtained by gluing suitable logical frameworks from the components. Show more
Keywords: dynamic agents, synchronization, categorical semantics, models of concurrent, distributed and mobile computing, system specification
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 19-33, 2008
Authors: Bellia, Marco | Occhiuto, M. Eugenia
Article Type: Research Article
Abstract: The paper investigates the use of preprocessing in adding higher order functionalities to Java, that is in passing methods to other methods. The approach is based on a mechanism which offers a restricted, disciplined, form of abstraction that is suitable to the integration of high order and object oriented programming. We show how this integration can be exploited in programming through the development of an example. Then, we discuss how the expressive power of the language …is improved. A new syntax is introduced for formal and actual parameters, hence the paper defines a translation that, at preprocessing time, maps programs of the extended language into programs of ordinary Java. Show more
Keywords: Higher order programming, object oriented programming, preprocessing
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 35-50, 2008
Authors: Budzyńska, Katarzyna | Kacprzak, Magdalena
Article Type: Research Article
Abstract: In the article, we introduce a sound and complete deductive system (AGn) which can be used to reason about persuasion process performed in distributed systems of agents in circumstances of uncertain and incomplete information. In order to express degrees of beliefs of these agents, we adopt methods of Logic of Graded Modalities. To represent degrees' changes resulting from the persuasion, we apply tools of Algorithmic Logic and Dynamic Logic. As a result, we interpret arguments as …actions which lead to change of grades of agents' beliefs. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 51-65, 2008
Authors: Chrz�stowski-Wachtel, Piotr | Findeisen, Paweł | Wolny, Grzegorz
Article Type: Research Article
Abstract: Workflows with transition execution times having exponential distributions are considered. The aim is to determine the overall execution time without looking into the reachability space and its analysis using Markov processes. We concentrate on the so called structural workflows, which are represented with Petri nets constructed by means of specific refinement rules. With each refinement rule (sequence, choice, parallelization, loop) we associate formulas which allow to compute the overall execution time distribution. …The class of exponential distributions is too narrow to keep the result within itself. We analyze the so called exponential polynomials, generalizing exponential distributions. They are closed under SUM and MAX functions. This closure property combined with the knowledge of refinements history enables us to find the requested formulas. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 67-87, 2008
Authors: Czaja, Ludwik
Article Type: Research Article
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 89-95, 2008
Authors: Delimata, Pawel | Suraj, Zbigniew
Article Type: Research Article
Abstract: Many problems in pattern classification and knowledge discovery require a selection of a subset of attributes or features to represent the patterns to be classified. The approach presented in this paper is designed mostly for multiple classifier systems with homogeneous (identical) classifiers. Such systems require many different subsets of the data set. The problem of finding the best subsets of a given feature set is of exponential complexity. The main aim of this paper is to …present ways to improve RBFS algorithm which is a feature selection algorithm. RBFS algorithm is computationally quite complex because it uses all decision-relative reducts of a given decision table. In order to increase its speed, we propose a new algorithm called ARS algorithm. The task of this algorithm is to decrease the number of the decision-relative reducts for a decision table. Experiments have shown that ARS has greatly improved the execution time of the RBFS algorithm. A small loss on the classification accuracy of the multiple classifier used on the subset created by this algorithm has also been observed. To improve classification accuracy the simplified version of the bagging algorithm has been applied. Algorithms have been tested on some benchmarks. Show more
Keywords: feature selection, multiple classifiers, reducts, diversity measures
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 97-110, 2008
Authors: Farwer, Berndt | Jantzen, Matthias | Kudlek, Manfred | Rölke, Heiko | Zetzsche, Georg
Article Type: Research Article
Abstract: We present a generalization of finite automata using Petri nets as control, called Concurrent Finite Automata for short. Several modes of acceptance, defined by final markings of the Petri net, are introduced, and their equivalence is shown. The class of languages obtained by –free concurrent finite automata contains both the class of regular sets and the class of Petri net languages defined by final marking, and is contained in the class of context-sensitive languages.
Keywords: Finite automata, Petri nets
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 111-121, 2008
Authors: Göhring, Daniel | Mellmann, Heinrich | Gerasymova, Kataryna | Burkhard, Hans-Dieter
Article Type: Research Article
Abstract: Common approaches for robot navigation use Bayesian filters like particle filters, Kalman filters and their extended forms. We present an alternative and supplementing approach using constraint techniques based on spatial constraints between object positions. This yields several advantages. The robot can choose from a variety of belief functions, and the computational complexity is decreased by efficient algorithms. The paper investigates constraint propagation techniques under the special requirements of navigation tasks. Sensor data …are noisy, but a lot of redundancies can be exploited to improve the quality of the result. We introduce two quality measures: The ambiguity measure for constraint sets defines the precision, while inconsistencies are measured by the inconsistency measure. The measures can be used for evaluating the available data and for computing best fitting hypothesis. A constraint propagation algorithm is presented. Show more
Keywords: Robot Navigation, Constraints
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 123-137, 2008
Authors: Gomolińska, Anna
Article Type: Research Article
Abstract: In this article we discuss judgment of satisfiability of formulas of a knowledge representation language as an object classification task. Our viewpoint is that of the rough set theory (RST), and the descriptor language for Pawlak's information systems of a basic kind is taken as the study case. We show how certain analogy-based methods can be employed to judge satisfiability of formulas of that language.
Keywords: satisfiability of formulas, valuation, object classification, Pawlak's information system, descriptor language, analogy-based reasoning
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 139-153, 2008
Authors: Góra, Grzegorz | Kruczek, Piotr | Skowron, Andrzej | Bazan, Jan G. | Bazan-Socha, Stanisława | Pietrzyk, Jacek J.
Article Type: Research Article
Abstract: We discuss medical treatment planning in the context of case-based planning, where plans (of treatment) are treated as complex decisions. A plan for a particular case is constructed from known plans for similar training examples. In order to evaluate and improve the prediction quality of complex decisions, we use a method for approximation of similarity measure between plans. The method makes it possible to transform the acquired domain knowledge about similarities of plans, expressed by medical …experts in natural language, to a low level language understandable by the system. To accomplish this task, we developed a method for approximation of the ontology of concepts expressed by medical experts. We present two applications of the ontology approximation, namely, for approximation of similarity between patient histories and for approximation of compatibility of patient histories with planned therapies. Next, we use these concept approximations to define two measures on which are based two methods for (plan) therapy prediction. The article includes results of experiments with these methods performed on medical data obtained from Neonatal Intensive Care Unit, First Department of Pediatrics, Polish-American Institute of Pediatrics, Collegium Medicum, Jagiellonian University, Krak?ow, Poland. The experiments are pertained to the identification of infants' death risk caused by respiratory failure. Show more
Keywords: automated planning, ontology of concepts, respiratory failure, rough sets, ontology approximation, similarity relation approximation
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 155-172, 2008
Authors: Gruska, Damas P.
Article Type: Research Article
Abstract: A formal model for description of probabilistic timing attacks is presented and studied. It is based on a probabilistic timed process algebra, on observations (mappings which make visible only a part of system behavior) and on an information flow. The resulting security properties are studied and compared with other security concepts.
Keywords: probabilistic timed process algebras, timing attacks, information flow, opacity, security
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 173-187, 2008
Authors: Gruska, Damas P. | Maggiolo–Schettini, Andrea | Milazzo, Paolo
Article Type: Research Article
Abstract: Communicating Hierarchical Transaction-based Timed Automata have been introduced to model systems performing long–running transactions. Here, for these automata a security concept is introduced, which is based on a notion of opacity and on the assumption that an attacker can not only observe public system activities, but also cause abortion of some of them. Different intruder capabilities as well as different kinds of opacity are defined and the resulting security properties are investigated. Security of long–running …transactions is defined by the mentioned notion of opacity and conditions for compositionality are established. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 189-203, 2008
Authors: Grzymala-Busse, Jerzy W. | Rz�sa, Wojciech
Article Type: Research Article
Abstract: In this paper we discuss approximation spaces that are useful for studying local lower and upper approximations. Set definability and properties of the approximation space, including best approximations, are considered as well. Finding best approximations is a NP-hard problem. Finally, we present LEM2-like algorithms for determining local lower and upper coverings for a given incomplete data set. Lower and upper approximations, associated with these coverings, are sub-optimal.
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 205-217, 2008
Authors: van Hee, Kees | Serebrenik, Alexander | Sidorova, Natalia
Article Type: Research Article
Abstract: State of the art information system commonly record events in log files, also known as audit trails. Moreover, business processes often go beyond the sole recording the events and base decisions on the events observed in the past. To model such processes we extend the basic Petri net framework with the notion of history by associating tokens with histories, adding guards evaluated on the history to the transitions and mapping arcs to expressions involving histories. Guards …and arc expressions can involve data associated with the transitions. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 219-234, 2008
Authors: Janowska, Agata | Janowski, Paweł | Wróblewski, Dobiesław
Article Type: Research Article
Abstract: The aim of this work is to describe the translation from Intermediate Language, one of the input formalisms of the model checking platform VerICS, to timed automata with discrete data and to compare it with the translation to classical timed automata. The paper presents syntax and semantics of both formalisms, the translation rules as well as a simple example.
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 235-248, 2008
Authors: Jankowski, Andrzej | Peters, James F. | Skowron, Andrzej | Stepaniuk, Jaroslaw
Article Type: Research Article
Abstract: The problem considered in this paper is the evaluation of perception as a means of optimizing various tasks. The solution to this problem hearkens back to early research on rough set theory and approximation. For example, in 1982, Ewa Orłowska observed that approximation spaces serve as a formal counterpart of perception. In this paper, the evaluation of perception is at the level of approximation spaces. The quality of an approximation space relative to a given approximated …set of objects is a function of the description length of an approximation of the set of objects and the approximation quality of this set. In granular computing (GC), the focus is on discovering granules satisfying selected criteria. These criteria take inspiration from the minimal description length (MDL) principle proposed by Jorma Rissanen in 1983. In this paper, the role of approximation spaces in modeling compound granules satisfying such criteria is discussed. For example, in terms of approximation itself, this paper introduces an approach to function approximation in the context of a reinterpretation of the rough integral originally proposed by Zdzisław Pawlak in 1993. We also discuss some other examples of compound granule discovery problems that are related to compound granules representing process models and models of interaction between processes or approximation of trajectories of processes. All such granules should be discovered from data and domain knowledge. The contribution of this article is a proposed solution approach to evaluating perception that provides a basis for optimizing various tasks related to discovery of compound granules representing rough integrals, process models, their interaction, or approximation of trajectories of discovered models of processes. Show more
Keywords: Approximation space, description, function approximation, granule, granular computing, perception, quality of an approximation space, rough integral
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 249-265, 2008
Authors: Jantzen, Matthias | Kudlek, Manfred | Zetzsche, Georg
Article Type: Research Article
Abstract: This paper presents results regarding the various relations among the language classes defined by Concurrent Finite Automata, relations to other language classes, as well as decidability and closure properties.
Keywords: Finite automata, Petri nets, language classes
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 267-280, 2008
Authors: Jółkowska, Joanna | Ochmański, Edward
Article Type: Research Article
Abstract: We propose a trace-based approach to description behaviours of concurrent systems. First, we define the independency relation induced by arbitrary transition system, forming this way an asynchronous transition system. Then we introduce the notion of traceability of transition systems and study some decision problems, related to computing independency and deciding traceability for basic classes of Petri nets. Main results: traceability is decidable for place/transition nets and undecidable in broader classes of nets …– inhibitor, reset and transfer nets. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 281-295, 2008
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
Authors: Strzałka, Dominik | Grabowski, Franciszek
Article Type: Research Article
Abstract: This paper presents a preliminary analysis of the system behavior that works far from the thermodynamical equilibrium states in the environment with limited resources. The examples of such systems are the real computer systems. Nowadays in such systems the runoff characteristic of the information flow is very turbulent in contradiction to the current existing laminar models. These systems work under constant overload, which means a permanent thermodynamical non-equilibrium (from the thermodynamical point of view). For …such a situation the classical approach to their modeling is still based on Boltzmann-Gibbs (BG) thermodynamics,which is proper only for systems that are in equilibriumstate (sometimes called thermostatic) or very close to it. The changing number of tasks N in such systems and the limited resourcesK of the environment cause its chaotic behavior and generate the dependencies that have got a long-termproperty. Such processes degrade the system performance X and elongate the response time R; in other words degrade the Quality of Service (QoS). To understand the whole behavior of such systems one needs a proper thermodynamical basis that seems to be the Tsallis formula of the non-extensive entropy. Show more
Keywords: limited resources, non-extensive entropy, thermodynamic non-equilibrium
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 455-464, 2008
Authors: Varpaaniemi, Kimmo | Ojala, Leo
Article Type: Research Article
Abstract: Reachability analysis is one of the most successful methods used in design and validation of protocols for classical communication, whereas the predicate/transition-net formalism is one of the most appropriate formalisms for reachability analysis oriented modelling. Quantum teleportation and dense coding are non-classical communication protocols that have been widely researched in the field of quantum computing. In this article, we present predicate/transitionnet models of these two protocols and use the PROD reachability analysis tool for …analysing the models. Show more
Keywords: reachability analysis, predicate/transition-nets, quantum teleportation, dense coding
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 465-479, 2008
Authors: Winkowski, Józef
Article Type: Research Article
Abstract: The paper is devoted to characterizing systems with random behaviours. The characterization is based on considering systems in terms of their possible runs, called processes, where each process is represented by a pomset in an intrinsic, global time independent way and can possibly be obtained by composing sequentially and in parallel other processes.
Keywords: Universe of objects, processes, states, sequential composition, parallel composition, partial category, partial monoid, random behaviour
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 481-496, 2008
Authors: Wolski, Marcin
Article Type: Research Article
Abstract: In this paper we study metric properties of finite approximation spaces and approximation operators from Rough Set Theory. In the first part of the article we examine finite approximation spaces and finite approximation topological spaces regarded as particular instances of two basic types of information structures from the framework of Information Quanta: information quantum relational systems and property systems, respectively. In the second part of the paper is the Marczewski-Steinhaus metric discussed as a certain …distance of sets defined with respect to the approximation operators. We propose two types of á la Marczewski-Steinhaus distance functions: the first type is based on the lower approximation operator; the second one is based on the upper approximation operator. These types can be defined with respect to both finite approximation spaces (information quantum relational systems) and finite approximation topological spaces (property systems), giving us four distancemeasure functions. In order to define a distance of sets which preserves their lower and upper approximations, one can take the sum of two respective functions. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 497-512, 2008
Authors: Zbrzezny, Andrzej
Article Type: Research Article
Abstract: The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.
Keywords: ECTL, Bounded Model Checking, translation to SAT
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 513-531, 2008
Authors: Zbrzezny, Andrzej | Woźna, Bożena
Article Type: Research Article
Abstract: VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known …alternating bit protocol written in Java. Show more
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 533-548, 2008
Authors: Zielosko, Beata | Piliszczuk, Marcin
Article Type: Research Article
Abstract: In the paper the accuracy of greedy algorithmfor construction of partial tests (superreducts) and partial decision rules is considered. Results of experiments with greedy algorithm are described.
Keywords: Partial tests, partial reducts, partial decision rules, greedy algorithm
Citation: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 549-561, 2008
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
[email protected]
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office [email protected]
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
[email protected]
For editorial issues, like the status of your submitted paper or proposals, write to [email protected]
如果您在出版方面需要帮助或有任何建, 件至: [email protected]