Fundamenta Informaticae - Volume 101, issue 1-2

Authors: Czaja, Ludwik

Article Type: Other

DOI: 10.3233/FI-2010-270

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. v-v, 2010

Authors: Czaja, Ludwik | Kudlek, Manfred

Article Type: Research Article

Abstract: We extend the investigation of synthesis and analysis of net structures and transition graphs to such with inhibitor relations, and show that the results obtained for the simpler case can be extended, too.

DOI: 10.3233/FI-2010-271

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 1-7, 2010

Authors: Knapik, Michał | Penczek, Wojciech | Szreter, Maciej | , Agata | Półrola,

Article Type: Research Article

Abstract: Bounded Model Checking (BMC) is an efficient technique applicable to verification of temporal properties of (timed) distributed systems. In this paper we show for the first time how to apply BMC to parametric verification of time Petri nets with discrete-time semantics. The properties are expressed by formulas of the logic PRTECTL - a parametric extension of the existential fragment of Computation Tree Logic (CTL).

DOI: 10.3233/FI-2010-272

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 9-27, 2010

Authors: Köhler-Bußmeier, Michael | Heitmann, Frank

Article Type: Research Article

Abstract: In this paper we discuss the concept of safeness for Elementary Object Nets (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. Object nets are called elementary if the net system has a two levelled structure. The well known p/t nets can be considered as a special case of EOS. For p/t nets the concept of safeness means that there is at most one token on each place. Since object nets have nested markings there are different possibilities to generalise this idea for EOS. In this paper we define …different variants of EOS safeness, discuss their relationships, show that they all coincide for p/t-like EOS, and address the complexity of well known Petri net problems like reachability and liveness for this new class of object nets. Show more

DOI: 10.3233/FI-2010-273

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 29-43, 2010

Authors: Koutny, Maciej | Pietkiewicz-Koutny, Marta

Article Type: Research Article

Abstract: One of the possible ways of constructing concurrent systems is their automated synthesis from behavioural specifications. In this paper, we look at a particular instance of this approach which aims at constructing GALS (globally asynchronous locally synchronous) systems from specifications given in terms of transition systems with arcs labelled by steps of executed actions. GALS systems are represented by Elementary Net Systems with Localities (ENL-systems), each locality defining a set of co-located actions. The synthesis procedure is based on the regions of transition systems and we provide a number of criteria aimed at generating a minimal set of regions (conditions) …of an ENL-system generating a given transition system. Show more

Keywords: theory of concurrency, Petri nets, localities, analysis and synthesis, step sequence semantics, conflict, theory of regions, transition systems

DOI: 10.3233/FI-2010-274

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 45-58, 2010

Authors: Lomazova, Irina A.

Article Type: Research Article

Abstract: In this work we consider modeling of workflow systems with Petri nets. To increase flexibility and give tools for workflow models re-engineering we extend the formalism of workflow nets by considering systems of interacting nets. Then we study soundness – the main correctness property of workflow processes – and show, that for a special class of structured workflow system soundness can be proved in compositional way.

Keywords: Workflow modeling, Petri nets, soundness, compositionality

DOI: 10.3233/FI-2010-275

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 59-70, 2010

Authors: Lomuscio, Alessio | Penczek, Wojciech | Qu, Hongyang

Article Type: Research Article

Abstract: We investigate partial order reduction techniques for the verification of multi-agent systems. We investigate the case of interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed in the system. We present a notion of stuttering-equivalence and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing implementations …and the experimental results obtained against well-known examples in the MAS literature. Show more

DOI: 10.3233/FI-2010-276

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 71-90, 2010

Authors: Pałasiński, Marek | Pancerz, Krzysztof

Article Type: Research Article

Abstract: The aim of this paper is to give the basic view on computing consistent extensions and restrictions of information systems noting some order properties of information system families. Information systems are understood in the Pawlak’s sense as the systems of knowledge representation. The extension appears if we add to the original information system some new objects corresponding to the known attribute values. Analogously, the restriction appears if we remove from the original information system some objects. Presented observations enable us to find proper descriptions (preserving some features) of concurrent systems whose behavior is represented by means of information systems.

DOI: 10.3233/FI-2010-277

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 91-103, 2010

Authors: Redziejowski, Roman R.

Article Type: Research Article

Abstract: The construction of an associative ω-product of traces from an earlier paper is revisited using projection representation of traces. Using projections instead of trace prefixes results in very simple definitions and proofs.

DOI: 10.3233/FI-2010-278

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 105-113, 2010

Authors: Suraj, Zbigniew | Grochowalski, Piotr

Article Type: Research Article

Abstract: The main goal of this paper is to give the outline of some approach to intelligent searching the Rough Set Database System (RSDS). RSDS is a bibliographical system containing bibliographical descriptions of publications connected with methodology of rough sets and its applications. The presented approach bases on created ontologies which are models for the considered domain (rough set theory, its applications and related fields) and for information about publications coming from, for example, abstracts.

Keywords: ontology, rough sets, data mining, knowledge discovery, database systems

DOI: 10.3233/FI-2010-279

Citation: Fundamenta Informaticae, vol. 101, no. 1-2, pp. 115-123, 2010