Timed automata are a widely used formalism for specifying the discrete-state/continuous-time behavior of time-critical reactive systems. For the fundamental verification problem of comparing two timed automata, it has been shown that timed trace equivalence is undecidable, while timed bisimulation is decidable. The corresponding decidability proof uses region graphs, a finite but space-consuming characterization of timed automata semantics. Most verification tools use zone graphs instead, a symbolic and, on average, more space-efficient representation of timed automata semantics. However, zone graphs provide correct results only for those verification tasks that are reducible to reachability problems, and are too imprecise for timed bisimilarity checking. To the best of our knowledge, there is currently no practical tool for automated timed bisimilarity checking. In this paper, we propose a new representation of timed automata semantics that extends zone graphs by so-called virtual clocks. Our zone-based construction is, on average, significantly smaller than the corresponding region graph representation. We also present experimental results obtained by applying our tool implementation to timed automata models, which are often used to evaluate timed automata analysis techniques.
Structure connectivity and substructure connectivity are innovative indicators for assessing network reliability and fault tolerance. Similarly, fault diameter evaluates fault tolerance and transmission delays in networks. This paper extends the concept of fault diameter by introducing two new variants: structure fault diameter and substructure fault diameter, derived from structure connectivity and substructure connectivity respectively. For a connected graph G with W-structure connectivity κ(G;W) or W-substructure connectivity κ^s(G;W), the W-structure fault diameter D_f(G;W) and W-substructure fault diameter D_f^s(G;W) are defined as the maximum diameter of any subgraph of G resulting from removing up to κ(G;W)-1 W-structures or κ^s(G;W)-1 W-substructures. For the n-dimensional hypercube Q_n with n ≥ 3 and 1 ≤ m ≤ n - 2, we determine both D_f(Q_n;Q_m) and D_f^s(Q_n;Q_1). These findings generalize existing results for the diameter and fault diameter of Q_n, providing a broader understanding of the hypercube's structural properties under fault conditions.
Cycloids are particular Petri nets for modelling processes of actions and events, belonging to the fundaments of Petri's general systems theory. Defined by four parameters they provide an algebraic formalism to describe strongly synchronized sequential processes. To further investigate their structure, reduction systems of cycloids are defined in the style of rewriting systems and properties of irreducible cycloids are proved. In particular the synthesis of cycloid parameters from their Petri net structure is derived, leading to an efficient method for a decision procedure for cycloid isomorphism.
Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $\mu$MALL as a formal theory of arithmetic based on linear logic. This formal system is presented as a sequent calculus proof system that extends the standard proof system for multiplicative-additive linear logic (MALL) with the addition of the logical connectives universal and existential quantifiers (first-order quantifiers), term equality and non-equality, and the least and greatest fixed point operators. We first demonstrate how functions defined using $\mu$MALL relational specifications can be computed using a simple proof search algorithm. By incorporating weakening and contraction into $\mu$MALL, we obtain $\mu$LK+, a natural candidate for a classical sequent calculus for arithmetic. While important proof theory results are still lacking for $\mu$LK+ (including cut-elimination and the completeness of focusing), we prove that $\mu$LK+ is consistent and that it contains Peano arithmetic. We also prove some conservativity results regarding $\mu$LK+ over $\mu$MALL.
We establish various complexity results for the entailment problem between formulas in Separation Logic with user-defined predicates denoting recursive data structures. The considered fragments are characterized by syntactic conditions on the inductive rules that define the semantics of the predicates. We focus on so-called P-rules, which are similar to (but simpler than) the PCE rules introduced by Iosif et al. in 2013. In particular, for a specific fragment where predicates are defined by so-called loc-deterministic inductive rules, we devise a sound and complete cyclic proof procedure running in polynomial time. Several complexity lower bounds are provided, showing that any relaxing of the provided conditions makes the problem intractable.
We show that the equational theory of the structure ⟨ ω^ω: (x,y)↦ x+y, x↦ ωx ⟩ is finitely axiomatizable and give a simple axiom schema when the domain is the set of transfinite ordinals. We give an algorithm that given a pair of terms (E,F) decides in linear time with respect of their common length whether or not E=F is a consequence of the axioms.
We investigate the computational power of particle methods, a well-established class of algorit hms with applications in scientific computing and computer simulation. The computational power of a compute model determines the class of problems it can solve. Automata theory allows describing the computational power of abstract machines (automata) and the problems they can solve. At the top of the Chomsky hierarchy of formal languages and grammars are Turing machines, which resemble the concept on which most modern computers are built. Although particle methods can be interpreted as automata based on their formal definition, their computational power has so far not been studied. We address this by analyzing Turing completeness of particle methods. In particular, we prove two sets of restrictions under which a particle method is still Turing powerful, and we show when it loses Turing powerfulness. This contributes to understanding the theoretical foundations of particle methods and provides insight into the powerfulness of computer simulations.
Let $G$ be a graph and $S\subseteq V(G)$ with $|S|\geq 2$. Then the trees $T_1, T_2, \cdots, T_\ell$ in $G$ are\emph{internally disjoint Steiner trees} connecting $S$ (or $S$-Steiner trees) if$E(T_i) \cap E(T_j )=\emptyset$ and $V(T_i)\cap V(T_j)=S$ for everypair of distinct integers $i,j$, $1 \leq i, j \leq \ell$. Similarly,if we only have the condition $E(T_i) \cap E(T_j )=\emptyset$but without the condition $V(T_i)\cap V(T_j)=S$, then they are \emph{edge-disjointSteiner trees}.The \emph{generalized $k$-connectivity}, denoted by $\kappa_k(G)$,of a graph $G$, is defined as $\kappa_k(G)=\min\{\kappa_G(S)|S\subseteq V(G) \ \textrm{and} \ |S|=k \}$, where $\kappa_G(S)$ isthe maximum number of internally disjoint $S$-Steiner trees. The \emph{generalized local edge-connectivity}$\lambda_{G}(S)$ is the maximum number of edge-disjoint Steiner treesconnecting $S$ in $G$. The {\it generalized $k$-edge-connectivity}$\lambda_k(G)$ of $G$ is defined as$\lambda_k(G)=\min\{\lambda_{G}(S)\,|\,S\subseteq V(G) \ and \ |S|=k\}$.These measures aregeneralizations of the concepts of connectivity and edge-connectivity, and they and can be used as measuresof vulnerability of networks. It is, in general, difficult to compute these generalized connectivities. However, there are precise results for some special classes of graphs.In this paper, we obtain the exact value of $\lambda_{k}(S(n,\ell))$ for $3\leq k\leq \ell^n$, and the exact value of $\kappa_{k}(S(n,\ell))$ for $3\leq k\leq \ell$, where $S(n, \ell)$ is the Sierpi\'{n}ski graphs with order $\ell^n$. As a direct consequence, these graphs provide additional interesting examples when $\lambda_{k}(S(n,\ell))=\kappa_{k}(S(n,\ell))$. We also study the some network properties of Sierpi\'{n}ski graphs.
We introduce a just-in-time runtime program transformation strategy based on repeated recursion unfolding. Our online program optimization generates several versions of a recursion differentiated by the minimal number of recursive steps covered. The base case of the recursion is ignored in our technique. Our method is introduced here on the basis of single linear direct recursive rules. When a recursive call is encountered at runtime, first an unfolder creates specializations of the associated recursive rule on-the-fly and then an interpreter applies these rules to the call. Our approach reduces the number of recursive rule applications to its logarithm at the expense of introducing a logarithmic number of generic unfolded rules. We prove correctness of our online optimization technique and determine its time complexity. For recursions which have enough simplifyable unfoldings, a super-linear is possible, i.e. speedup by more than a constant factor. The necessary simplification is problem-specific and has to be provided at compile-time. In our speedup analysis, we prove a sufficient condition as well as a sufficient and necessary condition for super-linear speedup relating the complexity of the recursive steps of the original rule and the unfolded rules. We have implemented an unfolder and meta-interpreter for runtime repeated recursion unfolding with just five rules in Constraint Handling Rules (CHR) embedded in Prolog. We illustrate the feasibility of our approach with simplifications, time complexity results and benchmarks for some basic tractable algorithms. The simplifications require some insight and were derived manually. The runtime improvement quickly reaches several orders of magnitude, consistent with the super-linear speedup predicted by our theorems.
Reliability assessment of interconnection networks is critical to the design and maintenance of multiprocessor systems. The (n, k)-enhanced hypercube Q_n,k, as a variation of the hypercube Q_n, was proposed by Tzeng and Wei in 1991. As an extension of traditional edge-connectivity, h-extra edge-connectivity of a connected graph G, λ_h(G), is an essential parameter for evaluating the reliability of interconnection networks. This article intends to study the h-extra edge-connectivity of the (n,2)-enhanced hypercube Q_n,2. Suppose that the link malfunction of an interconnection network Q_n,2 does not isolate any subnetwork with no more than h-1 processors, the minimum number of these possible faulty links concentrates on a constant 2^n-1 for each integer ⌈11×2^n-1/48⌉≤ h ≤ 2^n-1 and n≥ 9. That is, for about 77.083% of values where h≤2^n-1, the corresponding h-extra edge-connectivity of Q_n,2, λ_h(Q_n,2), presents a concentration phenomenon. Moreover, the lower and upper bounds of h mentioned above are both tight.
A geodesic cover, also known as an isometric path cover, of a graph is a set of geodesics which cover the vertex set of the graph. An edge geodesic cover of a graph is a set of geodesics which cover the edge set of the graph. The geodesic (edge) cover number of a graph is the cardinality of a minimum (edge) geodesic cover. The (edge) geodesic cover problem of a graph is to find the (edge) geodesic cover number of the graph. Surprisingly, only partial solutions for these problems are available for most situations. In this paper we demonstrate that the geodesic cover number of the $r$-dimensional butterfly is $\lceil (2/3)2^r\rceil$ and that its edge geodesic cover number is $2^r$.
The categorical modeling of Petri nets has received much attention recently. The Dialectica construction has also had its fair share of attention. We revisit the use of the Dialectica construction as a categorical model for Petri nets generalizing the original application to suggest that Petri nets with different kinds of transitions can be modeled in the same categorical framework. Transitions representing truth-values, probabilities, rates or multiplicities, evaluated in different algebraic structures called lineales are useful and are modeled here in the same category. We investigate (categorical instances of) this generalized model and its connections to more recent models of categorical nets.
We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their typings.
The study of networks characteristics is an important subject in different fields, like math, chemistry, transportation, social network analysis etc. The residual closeness is one of the most sensitive measure of graphs vulnerability. In this article we calculate the link residual closeness of Harary graphs. Comment: 15 pages
In this paper we construct a new efficient updatable encryption (UE) scheme based on FrodoPKE learning with errors key encapsulation. We analyse the security of the proposed scheme in the backward-leak uni-directional setting within the rand-ind-eu-cpa model. Since the underlying computationally hard problem here is LWE, the scheme is secure against both classical and quantum attacks.
Miyaji, Nakabayashi, and Takano proposed the algorithm for the construction of prime order pairing-friendly elliptic curves with embedding degrees k=3,4,6. We present a method for generating generalized MNT curves. The order of such pairing-friendly curves is the product of two prime numbers.
This paper demonstrates that applying spin reversal transformations (SRT), commonly known as a sufficient method for privacy enhancement in problems solved using quantum annealing, does not guarantee privacy for all possible cases. We show how to recover the original problem from the Ising problem obtained using SRT when the resulting problem in Ising form represents the algebraic attack on the E_0 stream cipher. A small example illustrates how to retrieve the original problem from that transformed by SRT. Moreover, we show that our method is efficient also for full-scale problems.
Due to developments in quantum computing, classical asymmetric cryptography is at risk of being breached. Consequently, new Post-Quantum Cryptography (PQC) primitives using lattices are studied. Another point of scrutiny is the resilience of these new primitives to Side Channel Analysis (SCA), where an attacker can study physical leakages. In this work we discuss a SCA vulnerability due to the ciphertext malleability of some PQC primitives exposed by a work from Ravi et al. We propose a novel countermeasure to this vulnerability exploiting the same ciphertext malleability and discuss its practical application to several PQC primitives. We also extend the seminal work of Ravi et al. by detailing their attack on the different security levels of a post-quantum Key Encapsulation Mechanism (KEM), namely FrodoKEM. We also provide a generalisation of their attack to different parameters which could be used in future similar primitives.
We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples.
Analysis of a network in terms of vulnerability is one of the most significant problems. Graph theory serves as a valuable tool for solving complex network problems, and there exist numerous graph-theoretic parameters to analyze the system’s stability. Among these parameters, the closeness parameter stands out as one of the most commonly used vulnerability metrics. Its definition has evolved to enhance the ease of formulation and applicability to disconnected structures. Furthermore, based on the closeness parameter, vertex residual closeness, which is a newer and more sensitive parameter compared to other existing parameters, has been introduced as a new graph vulnerability index by Dangalchev. In this study, the outcomes of the closeness and vertex residual closeness parameters in Harary Graphs have been examined. Harary Graphs are well-known constructs that are distinguished by having n vertices that are k-connected with the least possible number of edges.
