Fundamenta Informaticae - Volume 130, issue 4

Authors: Akshay, S. | Bollig, Benedikt | Gastin, Paul | Mukund, Madhavan | Kumar, K. Narayan

Article Type: Research Article

Abstract: 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. Show more

Keywords: timed automata, distributed systems

DOI: 10.3233/FI-2014-996

Citation: Fundamenta Informaticae, vol. 130, no. 4, pp. 377-407, 2014

Authors: Elbassioni, Khaled | Hagen, Matthias | Rauf, Imran

Article Type: Research Article

Abstract: 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. Show more

Keywords: HBC-algorithm, MTminer, algorithm analysis, lower bound, transversal hypergraph generation

DOI: 10.3233/FI-2014-997

Citation: Fundamenta Informaticae, vol. 130, no. 4, pp. 409-414, 2014

Authors: Krzywkowski, Marcin

Article Type: Research Article

Abstract: We provide an algorithm for listing all minimal double dominating sets of a tree of order n in time $\mathcal{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.

Keywords: domination, double domination, minimal double dominating set, tree, combinatorial bound, exact exponential algorithm, listing algorithm

DOI: 10.3233/FI-2014-998

Citation: Fundamenta Informaticae, vol. 130, no. 4, pp. 415-421, 2014

Authors: Permpoontanalarp, Yongyuth | Sornkhom, Panupong

Article Type: Research Article

Abstract: 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. Show more

Keywords: Formal methods for cryptographic protocols, Model checking, Coloured Petri Nets, Petri Nets

DOI: 10.3233/FI-2014-999

Citation: Fundamenta Informaticae, vol. 130, no. 4, pp. 423-466, 2014

Authors: Wang, Xian-gyang | Niu, Pan-pan | Yang, Hong-ying | Zhang, Yan | Ma, Tian-xiao

Article Type: Research Article

Abstract: 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 then the 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. Show more

Keywords: Audio watermarking, desynchronization attack, Empirical Mode Decomposition, higher-order statistics, synchronization code

DOI: 10.3233/FI-2014-1000

Citation: Fundamenta Informaticae, vol. 130, no. 4, pp. 467-490, 2014

Article Type: Other

Citation: Fundamenta Informaticae, vol. 130, no. 4, pp. 491-492, 2014