Fundamenta Informaticae - Volume 125, issue 1

Authors: Abid, Chiheb Ameur | Zouari, Belhassen

Article Type: Research Article

Abstract: This paper deals with the modular analysis of distributed concurrent systems modelled by Petri nets. The main analysis techniques of such systems suffer from the well-known problem of the combinatory explosion of state space. In order to cope with this problem, we use a modular representation of the state space instead of the ordinary one. The modular representation, namely modular state space, is much smaller than the ordinary state space. We propose to distribute the modular state space on every machine associated with one module. We enhance the modularity of the verification of some local properties of any module by …limiting it to the exploration of local and some global information. Once the construction of the distributed state space is performed, there is no communication between modules during the verification. Show more

Keywords: Distributed systems, modular verification, Petri nets, state space explosion

DOI: 10.3233/FI-2013-850

Citation: Fundamenta Informaticae, vol. 125, no. 1, pp. 1-20, 2013

Authors: Felisiak, Mariusz

Article Type: Research Article

Abstract: By applying computer algebra tools (mainly, Maple and C++), given the Dynkin diagram $\Delta = \mathbb{A}_n$ , with n ≥ 2 vertices and the Euler quadratic form $q_\Delta : \mathbb{Z}^n \rightarrow \mathbb{Z}$ , we study the problem of classifying mesh root systems and the mesh geometries of roots of Δ (see Section 1 for details). The problem reduces to the computation of the Weyl orbits in the set $Mor_\Delta \subseteq \mathbb{M}_n(\mathbb{Z})$ of all matrix morsifications A of qΔ , i.e., the non-singular matrices $A \in \mathbb{M}_n(\mathbb{Z})$ such that (i) qΔ (v) = v · …A · vtr , for all $v \in \mathbb{Z}^n$ , and (ii) the Coxeter matrix CoxA := −A · A−tr lies in $Gl(n,\mathbb{Z})$ . The Weyl group $\mathbb{W}_\Delta \subseteq Gl(n, \mathbb{Z})$ acts on MorΔ and the determinant det $A \in \mathbb{Z}$ , the order cA ≥ 2 of CoxA (i.e. the Coxeter number), and the Coxeter polynomial $cox_A(t) := det(t \centerdot E \minus Cox_A) \in \mathbb{Z}[t]$ are $\mathbb{W}_\Delta$ -invariant. The problem of determining the $\mathbb{W}_\Delta$ -orbits $\cal{O}rb(A)$ of MorΔ and the Coxeter polynomials coxA (t), with $A \in Mor_\Delta$ , is studied in the paper and we get its solution for n ≤ 8, and $A = [a_{ij}] \in Mor_{\mathbb{A}}_n$ , with $\vert a_{ij} \vert \le 1$ . In this case, we prove that the number of the $\mathbb{W}_\Delta$ -orbits $\cal{O}rb(A)$ and the number of the Coxeter polynomials coxA (t) equals two or three, and the following three conditions are equivalent: (i) $\cal{O}rb(A) = \mathbb{O}rb(A\prime)$ , (ii) coxA (t) = coxA′ (t), (iii) cA · det A = cA′ · det A′. We also construct: (a) three pairwise different $\mathbb{W}_\Delta$ -orbits in MorΔ , with pairwise different Coxeter polynomials, if $\Delta = \mathbb{A}_{2m \minus 1}$ and m ≥ 3; and (b) two pairwise different $\mathbb{W}_\Delta$ -orbits in MorΔ , with pairwise different Coxeter polynomials, if $\Delta = \mathbb{A}_{2m}$ and m ≥ 1. Show more

DOI: 10.3233/FI-2013-851

Citation: Fundamenta Informaticae, vol. 125, no. 1, pp. 21-49, 2013

Authors: Kamide, Norihiro | Kaneiwa, Ken

Article Type: Research Article

Abstract: A logic called sequence-indexed linear logic (SLL) is proposed to appropriately formalize resource-sensitive reasoning with sequential information. The completeness and cut-elimination theorems for SLL are proved, and SLL and a fragment of SLL are shown to be undecidable and decidable, respectively. As an application of SLL, some specifications of secure password authentication systems are discussed.

Keywords: Linear logic, resource-sensitive reasoning, sequence modal operator, informational interpretation, completeness theorem, secure password authentication system

DOI: 10.3233/FI-2013-852

Citation: Fundamenta Informaticae, vol. 125, no. 1, pp. 51-70, 2013

Authors: Rotaru, Armand Stefan | Iftene, Sorin

Article Type: Research Article

Abstract: Atkin's algorithm [2] for computing square roots in $Z^*_p$ , where p is a prime such that p ≡ 5 mod 8, has been extended by Müller [15] for the case p ≡ 9 mod 16. In this paper we extend Atkin's algorithm to the general case p ≡ 2s + 1 mod 2s + 1, for any s ≥ 2, thus providing a complete solution for the case p ≡ 1 mod 4. Complexity analysis and comparisons with other methods are also provided.

Keywords: Square Roots, Efficient Computation, Complexity

DOI: 10.3233/FI-2013-853

Citation: Fundamenta Informaticae, vol. 125, no. 1, pp. 71-94, 2013

Authors: Tyszka, Apoloniusz

Article Type: Research Article

Abstract: Let En = {xi = 1; xi + xj = xk ; xi · xj = xk : i; j; k ∈ {1,...,n}}. We conjecture that if a system $S \subseteq E_n$ has only finitely many solutions in integers x1 ,...,xn , then each such solution (x1 ,...,xn ) satisfies |x1 |,...,|xn | ≤ 22n−1 . Assuming the conjecture, we prove: (1) there is an algorithm which to each Diophantine equation assigns an integer which is greater than the heights of integer (non-negative integer, rational) solutions, if these solutions form …a finite set, (2) if a set $\cal{M} \subseteq \mathbb{N}$ is recursively enumerable but not recursive, then a finite-fold Diophantine representation of $\cal{M}$ does not exist. Show more

Keywords: Davis-Putnam-Robinson-Matiyasevich theorem, Matiyasevich's conjecture on finite-fold Diophantine representations

DOI: 10.3233/FI-2013-854

Citation: Fundamenta Informaticae, vol. 125, no. 1, pp. 95-99, 2013