130 (1) 2014
- Logics, Agents, and Mobility. Extended Papers from the International Workshops LAM'10 and LAM'11 Preface i-i
- 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.
- 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.
- 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.
- 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.
- On the Computational Interpretation of CK_{n} for Contextual Information Processing
Michael Mendler, Stephan Scheele 125-162
We aim to establish the multi-modal logic CK_{n} 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 CK_{n}. The system CK_{n}
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 CK_{n} as a type theory
and introduce its computational λ-calculus, λCK_{n}. Extending previous
work on CK_{n}, 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 CK_{n} following the Curry-Howard
Correspondence. The associated modal type theory λCK_{n} permits an interpretation
for both the modalities ^{[¯]} and \Diamond of CK_{n} 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, λCK_{n} is suitable for proof search in CK_{n}.
At the same time, λCK_{n} 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, CK_{n} is not bound to a particular
contextual interpretation. Thus, λCK_{n} 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 λCK_{n}.
130 (2) 2014
- Computing and Communication Technologies. Preface i-iii
- 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(n^{2}) 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.
- 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.
- 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.
- 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(N^{3}), 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.
- 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.
- 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
- 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.
- 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.
- 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.3248^{n}). This implies that every tree has at most 1.3248^{n} minimal double dominating sets. We also show that this bound is tight.
- 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.
- 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.