Acta Informatica
Journal Prestige (SJR): 0.517 Citation Impact (citeScore): 1 Number of Followers: 5 Hybrid journal (It can contain Open Access articles) ISSN (Print) 14320525  ISSN (Online) 00015903 Published by SpringerVerlag [2468 journals] 
 Editorial 2023: changes and invariants

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
PubDate: 20231103

 A decision procedure for string constraints with string/integer conversion
and flat regular constraints
Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract String constraint solving is the core of various testing and verification approaches for scripting languages. Among algorithms for solving string constraints, flattening is a wellknown approach that is particularly useful in handling satisfiable instances. As string/integer conversion is an important function appearing in almost all scripting languages, Abdulla et al. extended the flattening approach to this function recently. However, their approach supports only a special flattening pattern and leaves the support of the general flat regular constraints as an open problem. In this paper, we fill the gap by proposing a complete flattening approach for the string/integer conversion. The approach is built upon a new quantifier elimination procedure for the linearexponential arithmetic (namely, the extension of Presburger arithmetic with exponential functions, denoted by ExpPA) improved from the one proposed by Cherlin and Point in 1986. We analyze the complexity of our quantifier elimination procedure and show that the decision problem for existential ExpPA formulas is in 3EXPTIME. Up to our knowledge, this is the first elementary complexity upper bound for this problem. While the quantifier elimination procedure is too expensive to be implemented efficiently, we propose various optimizations and provide a prototypical implementation. We evaluate the performance of our implementation on the benchmarks that are generated from the string hash functions as well as randomly. The experimental results show that our implementation outperforms the stateoftheart solvers.
PubDate: 20231024

 Discovering workflow nets of concurrent iterative processes

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract A novel and efficient method for discovering concurrent workflow processes is presented. It allows building a suitable workflow net (WFN) from a large event log \(\lambda \) , which represents the behaviour of complex iterative processes involving concurrency. First, the tinvariants are determined from \(\lambda \) ; this allows computing the causal and concurrent relations between the events and the implicit causal relations between events that do not appear consecutively in \(\lambda \) . Then a 1bounded WFN is built, which could be eventually adjusted if its tinvariants do not match with those computed from \(\lambda \) . The discovered model allows firing all the traces in \(\lambda \) . The procedures derived from the method are polynomial time on \( \lambda \) ; they have been implemented and tested on artificial logs.
PubDate: 20230914

 The second step in characterizing a threeword code

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract In the fields of combinatorics on words and theory of codes, a twoword language \(\{x, y\}\) is a code if and only if \(xy \not = yx\) . But up to now, corresponding characterizations for a threeword language, which forms a code, have not been completely found. Let \(X=\{x,\ y,\ z\}\) be a threeword language and \( x ,\ y ,\ z \) be their lengths. When \( x = y < z \) , a necessary and sufficient condition for X to be a code was obtained in 2018. If \( x < y = z \le 2 x \) , a necessary and sufficient condition for X to be a code is proposed in this paper.
PubDate: 20230908

 On firstorder runtime enforcement of branchingtime properties

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime for a specified operational model of enforcing monitors. We study the enforceability of branchingtime, firstorder properties expressed in the Hennessy–Milner Logic with Recursion ( \(\mu \) HML) with respect to monitors that can enforce behaviour involving events that carry data. To this end, we develop an operational framework for firstorder enforcement via suppressions, insertions and replacements. We then use this model to formalise the meaning of enforcing a branchingtime property. We also show that a safety syntactic fragment of the logic is enforceable within this framework by providing an automated synthesis function that generates correct suppression monitors from any formula taken from this logical fragment.
PubDate: 20230803
DOI: 10.1007/s00236023004419

 Dot to dot, simple or sophisticated: a survey on shape reconstruction
algorithms
Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract Dot pattern points are the samples taken from all regions of a 2D object, either inside or the boundary. Given a set of dot pattern points in the plane, the shape reconstruction problem seeks to find the boundaries of the points. These boundaries are not mathematically welldefined. Hence, a superior algorithm is the one which produces the result closest to the human visual perception. There are different challenges in designing these algorithms, such as the independence from human supervision, and the ability to detect multiple components, holes and sharp corners. In this paper, we present a thorough review on the rich body of research in shape reconstruction, classify the ideas behind the algorithms, and highlight their pros and cons. Moreover, to overcome the barriers of implementing these algorithms, we provide an integrated application to visualize the outputs of the prominent algorithms for further comparison.
PubDate: 20230801
DOI: 10.1007/s00236023004437

 Testing membership for timed automata

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract Given a timed automaton which admits thick components and a timed word w, we present a tester which decides if w is in the language of the automaton or if w is \(\epsilon \) far from the language, using finitely many samples taken from the weighted time distribution \(\mu \) associated with the input w. We introduce a distance between timed words, the timed edit distance, which generalizes the classical edit distance. A timed word w is \(\epsilon \) far from a timed language if its relative distance to the language is greater than \(\epsilon \) .
PubDate: 20230717
DOI: 10.1007/s00236023004428

 Simple chain automaton random number generator for IoT devices

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Random numbers are very important in many fields of computer science. Generating highquality random numbers using only basic arithmetic operations is challenging, especially for devices with limited hardware capabilities, such as Internet of Things (IoT) devices. In this paper, we present a novel pseudorandom number generator, the simple chain automaton random number generator (SCARNG), based on compositions of abstract automata. The main advantage of the presented algorithm is its simple structure that can be implemented easily for very low computing capacity IoT systems, FPGAs or GPU hardware. The generated random numbers demonstrate promising statistical behavior and satisfy the NIST statistical suite requirements, highlighting the potential of the SCARNG for practical applications.
PubDate: 20230608
DOI: 10.1007/s0023602300440w

 Weighted throughput in a single machine preemptive scheduling with
continuous controllable processing times
Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract We consider the problem of weighted throughput in the single machine preemptive scheduling with continuous controllable processing times. A set of tasks can be scheduled on a single machine. Each task j is associated with a nonnegative weight \(w_{j}\) , a release date, a due date, and an interval of possible processing times. A task j can either be scheduled with a total processing time \(p_j\) which is in the given interval, or rejected (not participating in the schedule). The reward for processing j for \(p_{j}\) time units is \(w_{j}p_{j}\) , and we are interested in constructing a feasible preemptive schedule such that the sum of rewards is maximized. We present a dynamic programming algorithm that solves the problem in pseudopolynomial time and use it to obtain an FPTAS. Afterward, as our main contribution we propose an interesting efficient frontier approach for improved complexity bounds.
PubDate: 20230601
DOI: 10.1007/s00236022004304

 Pushdown automata and constant height: decidability and bounds

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract It cannot be decided whether a pushdown automaton accepts using a pushdown height, which does not depend on the input length, i.e., when it accepts using constant height. Furthermore, when a pushdown automaton accepts in constant height, the height can be arbitrarily large with respect to the size of the description of the machine, namely it does not exist any recursive function in the size of the description of the machine bounding the height of the pushdown. In contrast, in the restricted case of pushdown automata over a oneletter input alphabet, i.e., unary pushdown automata, the situation is different. First, acceptance in constant height is decidable. Moreover, in the case of acceptance in constant height, the height is at most exponential with respect to the size of the description of the pushdown automaton. We also prove a matching lower bound. Finally, if a unary pushdown automaton uses nonconstant height to accept, then the height should grow at least as the logarithm of the input length. This bound is optimal.
PubDate: 20230601
DOI: 10.1007/s00236022004340

 Constrained polynomial zonotopes

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract We introduce constrained polynomial zonotopes, a novel nonconvex set representation that is closed under linear map, Minkowski sum, Cartesian product, convex hull, intersection, union, and quadratic as well as higherorder maps. We show that the computational complexity of the abovementioned set operations for constrained polynomial zonotopes is at most polynomial in the representation size. The fact that constrained polynomial zonotopes are generalizations of zonotopes, polytopes, polynomial zonotopes, Taylor models, and ellipsoids further substantiates the relevance of this new set representation. In addition, the conversion from other set representations to constrained polynomial zonotopes is at most polynomial with respect to the dimension, and we present efficient methods for representation size reduction and for enclosing constrained polynomial zonotopes by simpler set representations.
PubDate: 20230505
DOI: 10.1007/s00236023004375

 On the undecidability and descriptional complexity of synchronized regular
expressions
Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract In Freydenberger (Theory Comput Syst 53(2):159–193, 2013. https://doi.org/10.1007/s0022401293890), Freydenberger shows that the set of invalid computations of an extended Turing machine can be recognized by a synchronized regular expression [as defined in Della Penna et al. (Acta Informatica 39(1):31–70, 2003. https://doi.org/10.1007/s002360020099y)]. Therefore, the widely discussed predicate “ \(=\{0,1\}^*\) ” is not recursively enumerable for synchronized regular expressions (SRE). In this paper, we employ a stronger form of nonrecursive enumerability called productiveness and show that the set of invalid computations of a deterministic Turing machine on a single input can be recognized by a synchronized regular expression. Hence, for a polynomialtime decidable subset of SRE, where each expression generates either \(\{0, 1\}^*\) or \(\{0, 1\}^* \{w\}\) where \(w \in \{0, 1\}^*\) , the predicate “ \(=\{0,1\}^*\) ” is productive. This result can be easily applied to other classes of language descriptors due to the simplicity of the construction in its proof. This result also implies that many computational problems, especially promise problems, for SRE are productive. These problems include language class comparison problems (e.g., does a given synchronized regular expression generate a contextfree language'), and equivalence and containment problems of several types (e.g., does a given synchronized regular expression generate a language equal to a fixed unbounded regular set'). In addition, we study the descriptional complexity of SRE. A generalized method for studying tradeoffs between SRE and many classes of language descriptors is established.
PubDate: 20230410
DOI: 10.1007/s00236023004393

 Toward a theory of program repair

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract To repair a program does not mean to make it (absolutely) correct; it only means to make it morecorrect than it was originally. This is not a mundane academic distinction: given that programs typically have about a dozen faults per KLOC, it is important for program repair methods and tools to be designed in such a way that they map an incorrect program into a morecorrect, albeit still potentially incorrect, program. Yet in the absence of a concept of relative correctness, many program repair methods and tools resort to approximations of absolute correctness; since these methods and tools are often validated against programs with a single fault, making them absolutely correct is indistinguishable from making them morecorrect; this has contributed to conceal/obscure the absence of (and the need for) relative correctness. In this paper, we propose a theory of program repair based on a concept of relative correctness. We aspire to encourage researchers in program repair to explicitly specify what concept of relative correctness their method or tool is based upon; and to validate their method or tool by proving that it does enhance relative correctness, as defined.
PubDate: 20230327
DOI: 10.1007/s00236023004384

 Minimum status of trees with a given degree sequence

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract The minimum status (or its normalized version called proximity) is a wellknown concept in communication network theory. We determine the trees minimizing the minimum status among trees with a given degree sequence, and we show that the trees maximizing the minimum status among trees with a given degree sequence must be caterpillars with specific properties.
PubDate: 20230301
DOI: 10.1007/s00236022004162

 Reactive bisimulation semantics for a process algebra with timeouts

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with timeout transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.
PubDate: 20230301
DOI: 10.1007/s00236022004171

 Alternating complexity of counting firstorder logic for the subword order

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of firstorder logic by threshold counting quantifiers. The main result shows that the twovariable fragment of this logic can be decided in twofold exponential alternating time with linearly many alternations (and therefore in particular in twofold exponential space as announced in the conference version (Kuske and Schwarz, in: MFCS’20, Leibniz International Proceedings in Informatics (LIPIcs) vol. 170, pp 56:1–56:13. Schloss Dagstuhl  LeibnizZentrum für Informatik, 2020) of this paper) provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent in the space bound. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalises the procedure by Karandikar and Schnoebelen for firstorder logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.
PubDate: 20230301
DOI: 10.1007/s00236022004242

 Secretshared RAM indefinite private and secure RAM execution of perfectly
unrevealed programs
Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract Secure and private computations over random access machine (RAM) are preferred over computations with circuits or Turing machines. Secure RAM executions become more and more important in the scope of avoiding information leakage when executing programs over a single computer, as well as the clouds. In this paper, we proposed a novel scheme for evaluating RAM programs without revealing any information on the computation, including the program, the data, and the result. We use Shamir Secret Sharing to share all the program instructions and the private string matching technique to ensure the execution of the right instruction sequence. We stress that our scheme obtains informationtheoretical security and does not rely on any computational hardness assumptions.
PubDate: 20230301
DOI: 10.1007/s00236022004224

 On partial information retrieval: the unconstrained 100 prisoner problem

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract We consider a generalization of the classical 100 prisoner problem and its variant, involving empty boxes, whereby winning probabilities for a team depend on the number of attempts, as well as on the number of winners. We call this the unconstrained 100 prisoner problem. After introducing the 3 main classes of strategies, we define a variety of ‘hybrid’ strategies and quantify their winningefficiency. Whenever analytic results are not available, we make use of Monte Carlo simulations to estimate with high accuracy the winning probabilities. Based on the results obtained, we conjecture that all strategies, except for the strategy maximizing the winning probability of the classical (constrained) problem, converge to the random strategy under weak conditions on the number of players or empty boxes. We conclude by commenting on the possible applications of our results in understanding processes of information retrieval, such as “memory” in living organisms.
PubDate: 20221230
DOI: 10.1007/s0023602200436y

 From regular expression matching to parsing

Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract Given a regular expression R and a string Q, the regular expression parsing problem is to determine if Q matches R and if so, determine how it matches, i.e., by a mapping of the characters of Q to the characters in R. Regular expression parsing makes finding matches of a regular expression even more useful by allowing us to directly extract subpatterns of the match, e.g., for extracting IPaddresses from internet traffic analysis or extracting subparts of genomes from genetic data bases. We present a new general techniques for efficiently converting a large class of algorithms that determine if a string Q matches regular expression R into algorithms that can construct a corresponding mapping. As a consequence, we obtain the first efficient linear space solutions for regular expression parsing.
PubDate: 20221201
DOI: 10.1007/s00236022004206

 Decentralized runtime verification of message sequences in messagebased
systems
Free preprint version: Loading...Rate this result: What is this?Please help us test our new preprint finding feature by giving the preprint link a rating.
A 5 star rating indicates the linked preprint has the exact same content as the published article.
Abstract: Abstract Messagebased systems are usually distributed in nature, and distributed components collaborate via asynchronous message passing. In some cases, particular ordering among the messages may lead to violation of the desired properties such as data confidentiality. Due to the absence of a global clock and usage of offtheshelf components, such unwanted orderings can be neither statically inspected nor verified by revising their codes at design time. We propose a choreographybased runtime verification algorithm that given an automatabased specification of unwanted message sequences detects the formation of the unwanted sequences. Our algorithm is fully decentralized in the sense that each component is equipped with a monitor, as opposed to having a centralized monitor, and also the specification of the unwanted sequences is decomposed among monitors. In this way, when a component sends a message, its monitor inspects if there is a possibility for the formation of unwanted message sequences. As there is no global clock in messagebased systems, monitors cannot determine the exact ordering among messages. In such cases, they decide conservatively and declare a sequence formation even if that sequence has not been formed. We prevent such conservative declarations in our algorithm as much as possible and then characterize its operational guarantees. We evaluate the efficiency and scalability of our algorithm in terms of the communication overhead, the memory consumption, and the latency of the result declaration through simulation.
PubDate: 20221010
DOI: 10.1007/s0023602200435z
