80 (1-3) 2007

1. Antoni Mazurkiewicz - half a century of inspirational research - Preface i-ii
2. On First-Order Fragments for Mazurkiewicz Traces
   Volker Diekert, Martin Horsch, Manfred Kufleitner 1-29
   Mazurkiewicz traces form a model for concurrency. Temporal logic and first-order logic are important tools in order to deal with the abstract behavior of such systems. Since typical properties can be described by rather simple logical formulas one is interested in logical fragments.
   One focus of this paper is unary temporal logic and first-order logic in two variables. Over words, this corresponds to the variety of finite monoids called DA. However, over Mazurkiewicz traces it is crucial whether traces are given as dependence graphs or as partial orders (over words these notions coincide). The main technical contribution is a generalization of important characterizations of DA from words to dependence graphs, whereas the use of partial orders leads to strictly larger classes. As a consequence we can decide whether a first-order formula over dependence graphs is equivalent to a first-order formula in two variables. The corresponding result for partial orders is not known.
   This difference between dependence graphs and partial orders also affects the complexity of the satisfiability problems for the fragments under consideration: for first-order formulas in two variables we prove an NEXPTIME upper bound, whereas the corresponding problem for partial orders leads to EXPSPACE.
   Furthermore, we give several separation results for the alternation hierarchy for first-order logic. It turns out that even for those levels at which one can express the partial order relation in terms of dependence graphs, the fragments over partial orders have more expressive power.
3. On Preserving Structural and Behavioural Properties by Composing Net Systems on Interfaces
   Luca Bernardinello, Elena Monticelli, Lucia Pomello 31-47
   We study several properties of an operation which combines two net systems by identifying local states and synchronizing events according to morphisms towards an interface. We propose this operation as a tool for modular system design, where different components are required to comply with a shared interface, or protocol of communication. We prove results on the preservation of structural properties, expressed as invariants, and of behavioural properties, in particular of deadlock-freeness.
4. Formalising TCP's Data Transfer Service Language: A Symbolic Automaton and its Properties
   Jonathan Billington, Bing Han 49-74
   The TCP/IP protocol suite defines the procedures governing the movement of data within the Internet. A major component of the suite is the Transmission Control Protocol (TCP), which ensures data flows reliably between Internet applications. We use Coloured Petri Nets (CPNs) to model the application's view of the service provided by TCP for the transfer of data. This service depends on the storage capacity available in the Internet. We firstly establish exact expressions for the size of the CPN model's reachability graph (or state space) in terms of the storage capacity. They indicate that both the nodes and arcs of the state space grow exponentially in the storage capacity. Secondly, we derive a symbolic state space which represents an infinite family of state spaces, one for each value of the capacity. We prove that each member of this family is a strongly connected graph and that its associated finite state automaton is deterministic and minimum. Finally, we formulate the TCP data transfer service language for arbitrary capacity, from the symbolic representation of the family of automata. This service language is the yardstick against which the TCP data transfer protocol can be verified with respect to user observable sequences of events.
5. Making Petri Nets Safe and Free of Internal Transitions
   Eike Best, Philippe Darondeau, Harro Wimmel 75-90
   This paper discusses the following results: that bounded Petri nets can be transformed into pomset-equivalent safe nets; that bounded marked graphs can be transformed into step-language-equivalent safe marked graphs; that safe labelled marked graphs can be transformed into t-free safe labelled marked graphs; and that marked graphs can be separated. The paper also lists some open problems that have arisen in this context.
6. Static BiLog: a Unifying Language for Spatial Structures
   Giovanni Conforti, Damiano Macedonio, Vladimiro Sassone 91-110
   Aiming at a unified view of the logics describing spatial structures, we introduce a general framework, BiLog, whose formulae characterise monoidal categories. As a first instance of the framework we consider bigraphs, which are emerging as a an interesting (meta-)model for spatial structures and distributed calculi. Since bigraphs are built orthogonally on two structures, a hierarchical place graph for locations and a link (hyper-)graph for connections, we obtain a logic that is a natural composition of other two instances of BiLog: a Place Graph Logic and a Link Graph Logic. We prove that these instances generalise the spatial logics for trees, for graphs and for tree contexts. We also explore the concepts of separation and sharing in these logics. We note that both the operator * of Separation Logic and the operator | of spatial logics do not completely separate the underlying structures. These two different forms of separation can be naturally derived as instances of BiLog by using the complete separation induced by the tensor product of monoidal categories along with some form of sharing.
7. Finitary Compositions of Two-way Finite-State Transductions
   Joost Engelfriet, Hendrik Jan Hoogeboom 111-123
   The hierarchy of arbitrary compositions of two-way nondeterministic finite-state transductions collapses when restricted to finitary transductions, i.e., transductions that produce a finite set of outputs for each input. The hierarchy collapses to the class of nondeterministic mso definable transductions, which is inside the second level of that hierarchy. It is decidable whether a composition of two-way nondeterministic finite-state transducers realizes a finitary transduction (i.e., is mso definable).
8. Computing Properties of Numerical Imperative Programs by Symbolic Computation
   Jacques Carette, Ryszard Janicki 125-146
   We show how properties of an interesting class of imperative programs can be calculated by means of relational modeling and symbolic computation. The ideas of [5, 26] are implemented using symbolic computations based on Maple [30].
9. On Communicating Automata with Bounded Channels
   Blaise Genest, Dietrich Kuske, Anca Muscholl 147-167
   We review the characterization of communicating finite-state machines whose behaviors have universally or existentially bounded channels. These results rely on the theory of Mazurkiewicz traces. We investigate the question whether channel bound conditions are decidable for a given communicating finite-state machine.
10. Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces
    Paul Gastin, Dietrich Kuske 169-197
    We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.
11. Processes of Petri Nets with Range Testing
    Jetty Kleijn, Maciej Koutny 199-219
    We are concerned with causality semantics in the executions of Petri nets with range arcs. Range arcs combine (and subsume) the distinctive features of inhibitor and activator arcs, and each such arc provides a means of specifying a range (a finite or infinite interval of non-negative integers) for the number of tokens in a place which makes enabling of a given transition possible. We demonstrate that the existing treatment of causality developed for Petri nets with inhibitor arcs based on structures generalising partial orders can also be applied to nets with range arcs.
12. An Efficient Message Passing Election Algorithm based on Mazurkiewicz's Algorithm
    Jérémie Chalopin, Yves Métivier 221-246
    We study the election and the naming problems in the asynchronous message passing model. We present a necessary condition based on Angluin's lifting lemma [1] that must be satisfied by any network that admits a naming (or an election) algorithm. We then show that this necessary condition is also sufficient: we present an election and naming algorithm based on Mazurkiewicz's algorithm [17]. The algorithm we obtained is totally asynchronous and it needs a polynomial number of messages of polynomial size, whereas previous election algorithms in this model are pseudo-synchronous and use messages of exponential size.
13. On Minimal Rule Sets for Almost All Binary Information Systems
    Mikhail Ju. Moshkov, Andrzej Skowron, Zbigniew Suraj 247-258
    The minimal rules for information systems are often used for inducing data models by methods in which the optimization of models is based on the minimal length principle. We show that almost all information systems from a certain large class of information systems have relatively short minimal rules. However, the number of such rules is not polynomial in the number of attributes and the number of objects. This class consists of all binary information systems with the number of objects polynomial in the number of attributes. Hence, for efficient inducing data models some filtration techniques in rule generation are necessary. In our further study we would like to extend our results for arbitrary information systems.
14. On Ethics of Mazurkiewicz Traces
    Edward Ochmański, Joanna Pieckowska 259-272
    We extend the well-known hierarchy ¥-fair Í 0-fair Í just for sequences (sequential computations) to that of traces (concurrent processes). The fairness hierarchy for traces is similar, but more involved than for sequences. We study this hierarchy, first in general, abstracting from concrete concurrent system, then for basic classes of Petri nets - elementary and place/transition nets. Finally, we define the fairness notions in a non-interleaving way and compare them with the former ones.
15. The Decent Philosophers: An Exercise in Concurrent Behaviour
    Wolfgang Reisig 273-281
    Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.
16. On Process-algebraic Verification of Asynchronous Circuits
    Xu Wang, Marta Kwiatkowska 283-310
    Asynchronous circuits have received much attention recently due to their potential for energy savings. Process algebras have been extensively used in the modelling, analysis and synthesis of asynchronous circuits. This paper develops a theoretical basis for using process algebra and associated model checking tools to verify asynchronous circuits. We formulate a model that extends existing verification theory for asynchronous circuits, and integrate it into the framework of standard process algebra theory. Our theory permits analysis of safeness (i.e. choke) and progress (i.e. illegal stop, divergence and relative starvation) conditions. We show how the model can be translated into CSP, and how the satisfaction of safeness and progress requirements can be reduced to refinement checks in CSP. Finally, the correspondence of our theory with trace theory (i.e. prefix-closed trace structures), receptive process theory and the XDI model is investigated.
17. Towards a Framework for Modelling Behaviours of Hybrid Systems
    Józef Winkowski 311-332
    The paper is devoted to characterizing hybrid systems by specifying 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.

80 (4) 2007

1. Maurer Computers with Single-Thread Control
   Jan A. Bergstra, Cornelis A. Middelburg 333-362
   We investigate basic issues concerning stored threads and their execution, building upon Maurer's model for computers and the thread algebra of Bergstra et al. We show among other things that a single thread can control the execution on a Maurer machine of any executable finite-state thread stored in the memory of the Maurer machine. We also relate stored threads with programs as considered in the program algebra of Bergstra et al. The work is intended as a preparation for the development of a formal approach to model micro-architectures and to verify their correctness and anticipated speed-up results.
2. How to Compute Times of Random Walks based Distributed Algorithms
   Alain Bui, Devan Sohier 363-378
   Random walk based distributed algorithms make use of a token that circulates in the system according to a random walk scheme to achieve their goal. To study their efficiency and compare it to one of the deterministic solutions, one is led to compute certain quantities, namely the hitting times and the cover time. Until now, only bounds on these quantities were known.
   First, this paper presents two generalizations of the notions of hitting and cover times to weighted graphs. Indeed, the properties of random walks on symmetrically weighted graphs provide interesting results on random walk based distributed algorithms, such as local load balancing. Both of these generalizations are proposed to precisely represent the behaviour of these algorithms, and to take into account what the weights represent.
   Then, we propose an algorithm to compute the n² hitting times on a weighted graph of n vertices, which we improve to obtain a O(n³) complexity. This complexity is the lowest up to now. This algorithm computes both of the generalizations that we propose for the hitting times on a weighted graph.
   Finally, we provide the first algorithm to compute the cover time (in both senses) of a graph. We improve it to achieve a complexity of O(n³2ⁿ). The algorithms that we present are all robust to a topological change in a limited number of edges. This property allows us to use them on dynamic graphs.
3. Inference of Parsable Graph Grammars for Syntactic Pattern Recognition
   Mariusz Flasiński 379-413
   A research into a syntactic pattern recognition model based on ( edNLC) graph grammars (introduced and investigated in Janssens and Rozenberg Inform. Sci. 20 (1980), 191-216, and Janssens, Rozenberg and Verraedt Comp. Vis. Graph. Image Process. 18 (1982), 279-304) has resulted in defining the efficient, O(n²), parsing schemes for the ETPL(k) subclass of these grammars and applying it for scene analysis, CAD/CAM object analysis and constructing AI systems (Flasiński Patt. Recogn. 21 (1988), 623-629, Flasiński Comp. Vis. Graph. Image Process. 47 (1989), 1-21, Flasiński Patt. Recogn. 26 (1993), 1-16, Flasiński Comp. Aided-Des. 27 (1995), 403-433, Flasiński Theor. Comp. Sci. 201 (1998), 189-231). In the paper the grammatical inference method for the parsable ETPL(k) graph grammars is defined, completing the development of this syntactic pattern recognition model.
4. A Data Mining Formalization to Improve Hypergraph
   Minimal Transversal Computation
   Céline Hébert, Alain Bretto, Bruno Crémilleux 415-433
   Finding hypergraph transversals is a major algorithmic issue which was shown having many connections with the data mining area. In this paper, by defining a new Galois connection, we show that this problem is closely related to the mining of the so-called condensed representations of frequent patterns. This data mining formalization enables us to benefit from efficient algorithms dedicated to the extraction of condensed representations. More precisely, we demonstrate how it is possible to use the levelwise framework to improve the hypergraph minimal transversal computation by exploiting an anti-monotone constraint to safely prune the search space. We propose a new algorithm MTminer to extract minimal transversals and provide experiments showing that our method is efficient in practice.
5. Formal Concept Analysis in Relational Database and Rough Relational Database
   Feng Jiang, Yuefei Sui and Cungen Cao 435-451
   Since its foundation in the early 1980's, Formal Concept Analysis (FCA) has been used in many applications in data analysis, information retrieval, and knowledge discovery. In this paper, we suggest to exploit the framework of relational database model (RDM) and rough relational database model (RRDM) for Formal Concept Analysis. The basic idea is as follows. We firstly treat any relation (R,A) of RDM as a many-valued context of FCA. But for the rough relations of RRDM, we define a special kind of many-valued context - rough-relational context in FCA (In this kind of context, every attribute value is a subset, but not an element, of the corresponding attribute domain), and treat any rough relation (R,A) of RRDM as a rough-relational context of FCA. Correspondingly, the definitions for concepts or rough concepts in context or rough-relational context (R,A) are given. The basic properties about these concepts or rough concepts in (R,A) are also discussed.
6. Security Analysis of the Pomykała-Barabasz Scheme
   Fagen Li, Yupu Hu 453-462

   In 2006, Pomykala and Barabasz [Fundamenta Informaticae 69 (2006) 411–425] proposed an elliptic curve based threshold proxy signature scheme which requires shorter cryptographic keys.They claimed that their scheme satisfies the secrecy, the proxy protected, the unforgeability, the non-repudiation, and the known signers. However, in this paper, we show that their scheme cannot achieve the proxy protected, the unforgeability and the non-repudiation by demonstrating a conspiracy attack. In this attack, any t malicious proxy signers can collusively impersonate some other proxy signers to generate proxy signatures
7. A New Practical Limited Identity-Based Encryption Scheme
   Rongxing Lu, Zhenfu Cao, Xiaolei Dong 463-476
   Identity based cryptography was introduced by Shamir in 1984, which avoids the trust problems encountered in the traditional Public Key Infrastructures. After Boneh and Franklin proposed the first full functional identity based encryption scheme from the bilinear pairings in 2001, many other identity based schemes using pairings have been proposed. However, how to design a practical identity based encryption scheme that avoids using the pairings is still an open problem today. In this paper, after studying and combining the advantages of the traditional public key system and identity based system, we formally define a new Limited identity based system and present a concrete Limited identity based encryption scheme on a different complexity assumption. The resulting scheme is not only provably secure against the chosen plaintext attack in the random oracle, but also especially suitable for some practical system, such as an email system.
8. RFCM: A Hybrid Clustering Algorithm Using Rough and Fuzzy Sets
   Pradipta Maji and Sankar K. Pal 477-498
   A hybrid unsupervised learning algorithm, termed as rough-fuzzy c-means, is proposed in this paper. It comprises a judicious integration of the principles of rough sets and fuzzy sets. While the concept of lower and upper approximations of rough sets deals with uncertainty, vagueness, and incompleteness in class definition, the membership function of fuzzy sets enables efficient handling of overlapping partitions. The concept of crisp lower bound and fuzzy boundary of a class, introduced in rough-fuzzy c-means, enables efficient selection of cluster prototypes. Several quantitative indices are introduced based on rough sets for evaluating the performance of the proposed c-means algorithm. The effectiveness of the algorithm, along with a comparison with other algorithms, has been demonstrated on a set of real life data sets.