130 (1) 2014

  1. Logics, Agents, and Mobility. Extended Papers from the International Workshops LAM'10 and LAM'11  Preface i-i
  2. Synthesis of Reo Connectors for Strategies and Controllers
    Christel Baier,  Joachim Klein,  Sascha Klüppelholz 1-20
    In controller synthesis, i.e., the question whether there is a controller or strategy to achieve some objective in a given system, the controller is often realized as some kind of automaton. In the context of the exogenous coordination language Reo, where the coordination glue code between the components is realized as a network of channels, it is desirable for such synthesized controllers to also take the form of a Reo connector built from a repertoire of basic channels. In this paper, we address the automatic construction of such Reo connectors directly from a constraint automaton representation.
  3. On the π-calculus and Co-intuitionistic Logic. Notes on Logic for Concurrency
    and λP Systems

    Gianluigi Bellin,  Alessandro Menti 21-65
    We reconsider work by Bellin and Scott in the 1990s on R. Milner and S. Abramsky's encoding of linear logic in the π-calculus and give an account of efforts to establish a tight connection between the structure of proofs and of the cut elimination process in multiplicative linear logic, on one hand, and the input-output behaviour of the processes that represent them, on the other, resulting in a proof-theoretic account of (a variant of) Chu's construction. But Milner's encoding of the linear lambda calculus suggests consideration of multiplicative co-intuitionistic linear logic: we provide a term assignment for it, a calculus of coroutines which presents features of concurrent and distributed computing. Finally, as a test case of its adequacy as a logic for distributed computation, we represent our term assignment as a λP system. We argue that translations of typed functional languages in concurrent and distributed systems (such as π-calculi or λP systems) are best typed with co-intuitionistic logic, where some features of computations match the logical properties in a natural way.
  4. Substructural Meta-Theory of a Type-Safe Language for Web Programming
    Iliano Cervesato,  Thierry Sans 67-97
    This paper introduces an abstract web programming language, QWeSST, and a methodology for proving properties of formalisms, such are QWeSST, that are parallel, distributed and concurrent. At its core, QWeSST is a small functional programming language extended with primitives for mobile code and remote procedure calls, two distinguishing features of web programming. It supports a localized view of typechecking and of evaluation, which reflects the way we program web applications and web services. We have developed a prototype implementation for QWeSST and used it to elegantly write simple web applications that are however not easily expressed using current web technology. We give two semantics for QWeSST, one is standard and models a naive form of single-threaded evaluation, the other is maximally parallel and exploits a presentation of its typing and execution behaviors based on an extended form of substructural operational semantics. It augments standard inference rules with a construction that realizes parametric multiset comprehension, which makes it convenient to capture ensemble-level behaviors. We prove that both semantics are type safe, the former using traditional methods, the latter by developing a proof methodology that parallels the multiset-oriented presentation of the semantics.
  5. A Survey of Decidability Results for Elementary Object Systems
    Michael Köhler-Bußmeier 99-123
    This contribution presents recent results on 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 work we study the relationship of EOS to existing Petri net formalisms. It turns out that EOS are equivalent to counter programs.
    But even for the restricted subclass of conservative EOS reachability and liveness are undecidable problems. On the other hand for other properties like boundedness are still decidable for conservative EOS.
    We also study the sub-class of generalised state machines, which is worth mentioning since it combines decidability of many theoretically interesting properties with a quite rich practical modelling expressiveness.
  6. On the Computational Interpretation of CKn for Contextual Information Processing
    Michael Mendler,  Stephan Scheele 125-162
    We aim to establish the multi-modal logic CKn as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CKn. The system CKn  would then act as a core system for constructive contextual reasoning with controlled information flow.
    In this paper, as a first step towards this goal, we study CKn as a type theory and introduce its computational λ-calculus, λCKn. Extending previous work on CKn, we present a cut-free contextual sequent system in the spirit of Masini's two-dimensional generalisation of natural deduction and Brünnler's nested sequents and give a computational interpretation for CKn following the Curry-Howard Correspondence. The associated modal type theory λCKn permits an interpretation for both the modalities [¯] and \Diamond  of CKn as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, λCKn is suitable for proof search in CKn. At the same time, λCKn enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CKn is not bound to a particular contextual interpretation. Thus, λCKn constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to λCKn.

130 (2) 2014

  1. Computing and Communication Technologies.  Preface i-iii
  2. Quadratic Algorithms for Testing of Codes and -Codes
    Nguyen Dinh Han,  Ho Ngoc Vinh,  Dang Quyet Thang, Phan Trung Huy 163-177
    The Sardinas-Patterson's test for codes has contributed many effective testing algorithms to the development of theory of codes, formal languages, etc. However, we will show that a modification of this test proposed in this paper can deduce more effective testing algorithms for codes. As a consequence, we establish a quadratic algorithm that, given as input a regular language X defined by a tuple (φ,M,B), where φ: A* → M is a monoid morphism saturating X, M is a finite monoid, B ⊆ M, X=φ−1(B), decides in time complexity O(n2) whether X is a code, where n= Card(M). Specially, n can be chosen as the finite index of X. A quadratic algorithm for testing of ◊-codes is also established.
  3. An Efficient Framework for Extracting Parallel Sentences from Non-Parallel Corpora
    Cuong Hoang,  Anh-Cuong Le,  Phuong-Thai Nguyen,  Son Bao Pham,  Tu Bao Ho 179-199
    Automatically building a large bilingual corpus that contains millions of words is always a challenging task. In particular in case of low-resource languages, it is difficult to find an existing parallel corpus which is large enough for building a real statistical machine translation. However, comparable non-parallel corpora are richly available in the Internet environment, such as in Wikipedia, and from which we can extract valuable parallel texts. This work presents a framework for effectively extracting parallel sentences from that resource, which results in significantly improving the performance of statistical machine translation systems. Our framework is a bootstrapping-based method that is strengthened by using a new measurement for estimating the similarity between two bilingual sentences. We conduct experiment for the language pair of English and Vietnamese and obtain promising results on both constructing parallel corpora and improving the accuracy of machine translation from English to Vietnamese.
  4. Unsupervised and Interactive Semi-supervised Clustering for Large Image Database Indexing and Retrieval
    Hien Phuong Lai,  Muriel Visani,  Alain Boucher,  Jean-Marc Ogier 201-218
    The feature space structuring methods play a very important role in finding information in large image databases. They organize indexed images in order to facilitate, accelerate and improve the results of further retrieval. Clustering, one kind of feature space structuring, may organize the dataset into groups of similar objects without prior knowledge (unsupervised clustering) or with a limited amount of prior knowledge (semi-supervised clustering). In this paper, we present both formal and experimental comparisons of different unsupervised clustering methods for structuring large image databases. We use different image databases of increasing sizes (Wang, PascalVoc2006, Caltech101, Corel30k) to study the scalability of the different approaches. Then, we present a new interactive semi-supervised clustering model, which allows users to provide feedback in order to improve the clustering results according to their wishes. Moreover, we also compare, experimentally, our proposed model with the semi-supervised HMRF-kmeans clustering method.
  5. A Better Heuristic Algorithm for Finding the Closest Trio of 3-colored Points from a Given Set of 3-colored Points on a Plane
    Ngoc Trung Nguyen,  Anh-Duc Duong 219-229
    We consider the following problem: Given n red points, m green points and p blue points on a plane, find a trio of red-green-blue points such that the distance between them is smallest. This problem could be solved by an exhaustive search algorithm: test all trios of 3 different colored points and find the closest trio. However, this algorithm has the complexity of O(N3), N=max(n,p,q). In our previous research, we already showed a heuristic algorithm with a good complexity to solve this problem based on 2D Voronoi diagram. In this paper, we introduce a better heuristic algorithm for solving this problem. This new heuristic algorithm has the same complexity but it performs much better than the old one.
  6. Heuristics to Solve a Real-world Asymmetric Vehicle Routing Problem with Side Constraints
    San Pham,  Viviane Gascon,  Tien Dinh 231-246
    To maintain patients at home as most as possible, healthcare services are nowadays quite diversified. We present the case of a public medical clinic offering activities, mostly to the elderly, at a daycare center. Users are brought into the daycare center by bus or by taxi. The global problem consists in defining routes to pick up users while assigning them to time slots in the week. At first sight this problem could be viewed as an asymmetric multiple vehicle routing problem. However many additional constraints must be considered. In this paper, we propose a metaheuristic including two phases to solve the problem. In the first phase, the initial solution is determined using one of two proposed constructed algorithms and is improved using tabu search in the second phase. These algorithms are tested on 10 problem instances. Experimental results are presented.
  7. Extraction of Discriminative Patterns from Skeleton Sequences for Accurate Action Recognition
    Tran Thang Thanh,  Fan Chen,  Kazunori Kotani, Bac Le 247-261
    Emergence of novel techniques devices e.g., MS Kinect, enables reliable extraction of human skeletons from action videos. Taking skeleton data as inputs, we propose an approach to extract the discriminative patterns for efficient human action recognition. Each action is considered to consist of a sequence of unit actions, each of which is represented by a pattern. Given a skeleton sequence, we first automatically extract the key-frames, and then categorize them into different patterns. We further use a statistical metric to evaluate the discriminative capability of patterns, and define them as local features for action recognition. Experimental results show that the extracted local descriptors could provide very high accuracy in the action recognition, which demonstrate the efficiency of our method in extracting discriminative unit actions.

130 (4) 2014

  1. Distributed Timed Automata with Independently Evolving Clocks
    S. Akshay,  Benedikt Bollig,  Paul Gastin,  Madhavan Mukund,  K. Narayan Kumar 377-407
    We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to.
    There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the existential semantics-the set of behaviors that the system can possibly exhibit under some choice of clock rates.
    We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors.
  2. A Lower Bound for the HBC Transversal Hypergraph Generation
    Khaled Elbassioni,  Matthias Hagen,  Imran Rauf 409-414
    The computation of transversal hypergraphs in output-polynomial time is a long standing open question. An Apriori-like level-wise approach (referred to as the HBC-algorithm or MTminer) was published in 2007 by Hébert, Bretto, and Crémilleux [A Data Mining Formalization to Improve Hypergraph Minimal Transversal Computation, Fundamenta Informaticae, 80(4), 2007, 415-433] and was experimentally demonstrated to have very good performance on hypergraphs with small transversals.
    In this short note extending the paper by Hagen [Lower bounds for three algorithms for transversal hypergraph generation, Discrete Applied Mathematics, 157(7), 2009, 1460-1469], we prove a superpolynomial lower bound for the HBC-algorithm. This lower bound also shows that the originally claimed upper bound on the HBC-algorithm's running time is wrong.
  3. An Algorithm for Listing all Minimal Double Dominating Sets of a Tree
    Marcin Krzywkowski 415-421
    We provide an algorithm for listing all minimal double dominating sets of a tree of order n in time O(1.3248n). This implies that every tree has at most 1.3248n minimal double dominating sets. We also show that this bound is tight.
  4. On-the-fly Trace Generation Approach to the Security Analysis of Cryptographic Protocols: Coloured Petri Nets-based Method
    Yongyuth Permpoontanalarp,  Panupong Sornkhom 423-466
    Most Petri nets-based methods that have been developed to analyze cryptographic protocols provide the analysis of one attack trace only. Only a few of them offer the analysis of multiple attack traces, but they are rather inefficient. Analogously, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. In this paper, we propose a very simple but practical Coloured Petri nets-based model checking method for the analysis of cryptographic protocols, which overcomes these limitations. Our method offers an efficient analysis of multiple attack traces. We apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali's contract signing protocol. Surprisingly, our simple method is very efficient when the numbers of attack traces and states are large. Also, we find many new attacks in those protocols.
  5. A Robust Audio Watermarking Scheme using Higher-order Statistics in Empirical Mode Decomposition Domain
    Xiang-yang Wang, Pan-pan Niu,  Hong-ying Yang,  Yan Zhang,  Tian-xiao Ma 467-490
    The development of a desynchronization invariant audio watermarking scheme without degrading acoustical quality is a challenging work. This paper proposes a robust audio watermarking scheme in Empirical Mode Decomposition (EMD) domain, in which the higher-order statistics and synchronization code are utilized. Firstly, the wavelet de-noising is performed on the original host audio, the de-noised digital audio is segmented, and then each segment is cut into two parts. Secondly, with the spatial watermarking technique, synchronization code is embedded into the statistics average value of audio samples in the first part. Thirdly, for the second part, EMD is performed, and a series of Intrinsic Mode Functions (IMFs) and a residual are given, and thenthe higher-order statistics of residual are obtained by using the Hausdorff distance. Finally, the digital watermark is embedded into the residual in EMD domain by using the higher-order statistics. Simulation results show that the proposed watermarking scheme is not only inaudible and robust against common signal processing operations such as MP3 compression, noise addition,resampling, and re-quantization etc, but also robust against the desynchronization attacks such as random cropping, amplitude variation, pitch shifting, and jittering etc.