Fundamenta Informaticae - Volume 120, issue 3-4

Authors: Penczek, Wojciech

Article Type: Other

DOI: 10.3233/FI-2012-757

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. i-i, 2012

Authors: De Angelis, Emanuele | Pettorossi, Alberto | Proietti, Maurizio

Article Type: Research Article

Abstract: We address the problem of the automatic synthesis of concurrent programs within a framework based on Answer Set Programming (ASP). Every concurrent program to be synthesized is specified by providing both the behavioural and the structural properties it should satisfy. Behavioural properties, such as safety and liveness properties, are specified by using formulas of the Computation Tree Logic, which are encoded as a logic program. Structural properties, such as the symmetry of processes, are also encoded as a logic program. Then, the program which is the union of these two encoding programs, is given as input to an ASP system …which returns as output a set of answer sets. Finally, each answer set is decoded into a synthesized program that, by construction, satisfies the desired behavioural and structural properties. Show more

DOI: 10.3233/FI-2012-758

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 205-229, 2012

Authors: Azad, Mohammad | Chikalov, Igor | Moshkov, Mikhail | Zielosko, Beata

Article Type: Research Article

Abstract: The paper is devoted to the study of a greedy algorithm for construction of approximate tests (super-reducts). This algorithm is applicable to decision tables with many-valued decisions where each row is labeled with a set of decisions. For a given row, we should find a decision from the set attached to this row. We consider bounds on the precision of this algorithm relative to the cardinality of tests.

Keywords: Decision table with many-valued decisions, test, reduct, greedy algorithm, set cover Problem

DOI: 10.3233/FI-2012-759

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 231-242, 2012

Authors: Bashkin, Vladimir A. | Lomazova, Irina A.

Article Type: Research Article

Abstract: Resource-driven automata (RDA) are finite automata, sitting in the nodes of a finite system net and asynchronously consuming/producing shared resources through input/output system ports (arcs of the system net). RDAs themselves may be resources for each other, thus allowing the highly flexible structure of the model. It was proved earlier, that RDA-nets are expressively equivalent to Petri nets [2]. In this paper the new formalism of cellular RDAs is introduced. Cellular RDAs are RDA-nets with an infinite regularly structured system net. We build a hierarchy of cellular RDA classes on the basis of restrictions on the underlying grid. The expressive …power of several major classes of 1-dimensional grids is studied. Show more

Keywords: multi-agent systems, mobile agents, Petri nets, cellular nets, Resource-Driven Automata

DOI: 10.3233/FI-2012-760

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 243-257, 2012

Authors: Drábik, Peter | Maggiolo-Schettini, Andrea | Milazzo, Paolo

Article Type: Research Article

Abstract: Property preservation is investigated as an approach to modular verification, leading to reduction of the property verification time for formal models. For modelling purposes, formalisms with multi-way synchronisations are considered. For the modular verification technique to work, a specific type of synchronisation is required for which a sufficient and necessary condition is identified. It is a requirement on the semantics of the formalism, which is restricted to permit simultaneous execution only of component moves that make reference to each other. Implications for modular verification of several well-known formalisms for concurrent systems are investigated.

Keywords: modular verification, synchronisation, automata

DOI: 10.3233/FI-2012-761

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 259-274, 2012

Authors: Dworzański, Leonid W. | Lomazova, Irina A.

Article Type: Research Article

Abstract: Nested Petri nets (NP-nets) are Petri nets with net tokens. The liveness and boundedness problems are undecidable for two-level NP-nets [14]. Boundedness is in EXPSPACE and liveness is in EXPSPACE or worse for plain Petri nets [6]. However, for some restricted classes, e.g. for plain free-choice Petri nets, problems become more amenable to analysis. There is a polynomial time algorithm to check if a free-choice Petri net is live and bounded [4]. In this paper we prove, that for NP-nets boundedness can be checked in a compositional way, and define restrictions, under which liveness is also compositional. These results give …a base to establish boundedness and liveness for NP-nets by checking these properties for separate plain components, which can belong to tractable Petri net subclasses, or be small enough for model checking. Show more

DOI: 10.3233/FI-2012-762

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 275-293, 2012

Authors: Gruska, Damas P.

Article Type: Research Article

Abstract: Formalisms for analysis of systems of various nature specified by process algebras are proposed. They allow us to formalize security properties based on an absence of information flow and properties on system's integrity. Resulting properties are compared and discussed. We present also quantification of these properties by means of information theory.

Keywords: information flow, opacity, nested attackers, information theory

DOI: 10.3233/FI-2012-763

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 295-309, 2012

Authors: Gruska, Damas P.

Article Type: Research Article

Abstract: Different techniques for expressing an amount of information on secrete data which can be obtained by a process observation are presented. They are based on information theory and they express certainty about sets of private actions which execution is guaranteed by a given observation and sets of actions which execution is excluded by a given observation. Moreover, the case when an intruder has same preliminary belief on secrete data is discussed. It is shown how the presented technique could be applied for such case. As regards working formalism, probabilistic process algebra is used for description of systems as well as …attacker's belief. Show more

Keywords: probabilistic process algebras, information flow, opacity, security, belief

DOI: 10.3233/FI-2012-764

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 311-324, 2012

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

Article Type: Research Article

Abstract: This contribution presents decidability results for the formalism of Elementary Object Systems (EOS). Object nets are Petri nets which have Petri nets as tokens – an approach known as the nets-within-nets paradigm. In this paper we study the relationship of the reachability and the liveness problem. We prove that both problems are undecidable for EOS (even for the subclass of conservative EOS) while it is well known that both are decidable for classical p/t nets. Despite these undecidability results, boundedness can be decided for conservative EOS using a monotonicity argument similar to that for p/t nets.

Keywords: Petri nets, nets-within-nets, nets as tokens, reachability, liveness, boundedness

DOI: 10.3233/FI-2012-765

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 325-339, 2012

Authors: Popova-Zeugmann, Louchka | Pelz, Elisabeth

Article Type: Research Article

Abstract: In this paper we consider Interval-Timed Petri nets (ITPN) which are an extension of Timed Petri nets. They are considered to behave with discrete delays. The class of ITPNs is Turing complete and therefore the reachability of an arbitrary marking in such a net is not decidable. We introduce a time dependent state equation for a firing sequence of ITPNs, which is analogous to the state equation for a firing sequence in standard Petri nets and we prove its correctness using linear algebra. Our result is original and delivers both a necessary condition for reachability and a sufficient condition for …non-reachability of an arbitrary marking in an ITPN. Show more

Keywords: Interval-Timed Petri nets, state equation, reachability, Interval-Timed Petri net analysis

DOI: 10.3233/FI-2012-766

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 341-357, 2012

Authors: Wiśniewski, Piotr | Burzańska, Marta | Stencel, Krzysztof

Article Type: Research Article

Abstract: In this paper we discuss the misunderstanding that have arisen over the years around the broadly defined term of the object-relational impedance mismatch. It occurs in various aspects of database application programming. There are three concerns judged the most important: mismatching data models, mismatching binding times and mismatching object lifecycle. This paper focuses on the data model mismatch. We introduce the common state theory, i.e. a unified model of objects in popular programming languages and databases. The proposed model exploits and emphasizes common properties of all these objects. Using our model we demonstrate that there are notably more similarities than …differences. We conclude that the impact of the mismatch of data models can be significantly reduced. Show more

Keywords: impedance mismatch, object-relational mapping, data models, object state

DOI: 10.3233/FI-2012-767

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 359-374, 2012

Authors: Zbrzezny, Andrzej

Article Type: Research Article

Abstract: In this paper we present a new translation from ECTL* to SAT and show that the proposed translation substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made experimental results, which demonstrate the efficiency of the method.

Keywords: ECTL*, translation to SAT, Bounded Model Checking

DOI: 10.3233/FI-2012-768

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 375-395, 2012

Article Type: Other

Citation: Fundamenta Informaticae, vol. 120, no. 3-4, pp. 397-398, 2012