We investigate the Sandpile Model and Chip Firing Game and an extension of these modelson cycle graphs. The extended model consists of allowing a negative number of chips ateach vertex. We give the characterization of reachable configurations and of fixed pointsof each model. At the end, we give explicit formula for the number of their fixedpoints.

Recently, Constantinescu and Ilie proved a variant of the well-known periodicity theoremof Fine and Wilf in the case of two relatively prime abelian periods and conjectured aresult for the case of two non-relatively prime abelian periods. In this paper, we answersome open problems they suggested. We show that their conjecture is false but we givebounds, that depend on the two abelian periods, such that the conjecture is true for allwords having length at least those bounds and show that some of them are optimal. We alsoextend their study to the context of partial words, giving optimal lengths and describingan algorithm for constructing optimal words.

We provide an algorithm for listing all minimal 2-dominating sets of a tree of ordern in time 𝒪(1.3248n). This implies that every tree has at most1.3248n minimal 2-dominating sets. We also show that thisbound is tight.

We prove the undecidability of Core XPath 1.0 (CXP) [G. Gottlob and C. Koch,inProc. of 17th Ann. IEEE Symp. on Logic in Computer Science,LICS ’02(Copenhagen,July 2002). IEEE CS Press (2002) 189–202.] extended with anInflationary Fixed Point (IFP) operator. More specifically,we provethat the satisfiability problem of this language is undecidable. In fact,the fragment ofCXP+IFP containing only the self and descendant axes is already undecidable.

We introduce a type of isomorphism among strategic games that we call localisomorphism. Local isomorphisms is a weaker version of the notions of strongand weak game isomorphism introduced in [J. Gabarro, A. Garcia and M. Serna,Theor. Comput. Sci. 412 (2011) 6675–6695]. In a localisomorphism it is required to preserve, for any player, the player’s preferences on thesets of strategy profiles that differ only in the action selected by this player. We showthat the game isomorphism problem for local isomorphism is equivalent to the same problemfor strong or weak isomorphism for strategic games given in: general, extensive andformula general form. As a consequence of the results in [J. Gabarro, A. Garcia and M.Serna, Theor. Comput. Sci. 412 (2011) 6675–6695] thisimplies that local isomorphism problem for strategic games is equivalent to (a) thecircuit isomorphism problem for games given in general form, (b) the boolean formulaisomorphism problem for formula games in general form, and (c) the graph isomorphismproblem for games given in explicit form.

A Message Authentication Code (MAC) is a function that takes a message and a key asparameters and outputs an authentication of the message. MAC are used to guarantee thelegitimacy of messages exchanged through a network, since generating a correctauthentication requires the knowledge of the key defined secretly by trusted parties.However, an attacker with access to a sufficiently large number of message/authenticationpairs may use a brute force algorithm to infer the secret key: from a set containinginitially all possible key candidates, subsequently remove those that yield an incorrectauthentication, proceeding this way for each intercepted message/authentication pair untila single key remains. In this paper, we determine an exact formula for the expected numberof message/authentication pairs that must be used before such form of attack issuccessful, along with an asymptotical bound that is both simple and tight. We conclude byillustrating a modern application where this bound comes in handy, namely the estimationof security levels in reflection-based verification of software integrity.

We describe a sequent calculus μLJ with primitives for inductive andcoinductive datatypes and equip it with reduction rules allowing a sound translation ofGödel’s system T. We introduce the notion of a μ-closedcategory, relying on a uniform interpretation of open μLJformulas as strong functors. We show that any μ-closed category is asound model for μLJ. We then turn to the construction of a concreteμ-closed category based on Hyland-Ong game semantics. The model relieson three main ingredients: the construction of a general class of strong functors calledopen functors acting on the category of games and strategies, thesolution of recursive arena equations by exploiting cycles in arenas, andthe adaptation of the winning conditions of parity games to build initial algebras andterminal coalgebras for many open functors. We also prove a weak completeness result forthis model, yielding a normalisation proof for μLJ.

We discuss how much space is sufficient to decide whether a unary given numbern is a prime. We show thatO(log log n) space is sufficient for a deterministicTuring machine, if it is equipped with an additional pebble movable along the input tape,and also for an alternating machine, if the space restriction applies only to itsaccepting computation subtrees. In other words, the language is a prime is inpebble–DSPACE(log log n) and also inaccept–ASPACE(log log n). Moreover, if the givenn is composite, such machines are able to find a divisor ofn. Since O(log log n) space is toosmall to write down a divisor, which might requireΩ(log n) bits, the witness divisor is indicated by theinput head position at the moment when the machine halts.

The cutwidth is an important graph-invariant in circuit layout designs. The cutwidth of agraph G is the minimum value of the maximum number of overlap edges whenG is embedded into a line. A caterpillar is a tree which yields a pathwhen all its leaves are removed. An iterated caterpillar is a tree which yields acaterpillar when all its leaves are removed. In this paper we present an exact formula forthe cutwidth of the iterated caterpillars.

A standard bridge between automata theory and logic is provided by the notion ofcharacteristic formula. This paper investigates this problem for the class ofevent-recording automata (ERA), a subclass of timed automata in which clocks areassociated with actions and that enjoys very good closure properties. We first study theproblem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), alogic introduced by Sorea to express event-based timed specifications. We prove that theconstruction proposed by Sorea for ERA without invariants is incorrect. More generally, weprove that timed bisimilarity cannot in general be expressed in ERL for the class of ERA ,and study under which conditions on ERA it can be. Then, we introduce the logicWTμ , a new logic for event-based timed specificationscloser to the timed logic ℒν that was introduced byLaroussinie, Larsen and Weise. We prove that it is strictly more expressive than ERL , andthat its model-checking problem against ERA is EXPTIME -complete. Finally, we providecharacteristic formulae constructions in WTμ forcharacterizing the general class of ERA up to timed (bi)similarity and study thecomplexity issues.

We give several new applications of the wreath product of forest algebras to the study oflogics on trees. These include new simplified proofs of necessary conditions fordefinability in CTL and first-order logic with the ancestor relation; asequence of identities satisfied by all forest languages definable inPDL; and new examples of languages outside CTL, alongwith an application to the question of what properties are definable in bothCTL and LTL.

The traveling salesman problem (TSP) is one of the most fundamental optimizationproblems. We consider the β-metric traveling salesman problem(Δβ-TSP), i.e., the TSPrestricted to graphs satisfying the β-triangle inequalityc({v,w}) ≤ β(c({v,u}) + c({u,w})),for some cost function c and any three vertices u,v,w.The well-known path matching Christofides algorithm (PMCA) guarantees an approximationratio of 3β2/2 and is the best known algorithm for theΔβ-TSP, for 1 ≤ β ≤ 2. Weprovide a complete analysis of the algorithm. First, we correct an error in the originalimplementation that may produce an invalid solution. Using a worst-case example, we thenshow that the algorithm cannot guarantee a better approximation ratio. The example canalso be used for the PMCA variants for the Hamiltonian path problem with zero and oneprespecified endpoints. For two prespecified endpoints, we cannot reuse the example, butwe construct another worst-case example to show the optimality of the analysis also inthis case.

We consider μ-calculus formulas in a normal form: after a prefix offixed-point quantifiers follows a quantifier-free expression. We are interested in theproblem of evaluating (model checking) such formulas in a powerset lattice. We assume thatthe quantifier-free part of the expression can be any monotone function given by ablack-box – we may only ask for its value for given arguments. As a first result we provethat when the lattice is fixed, the problem becomes polynomial (the assumption about thequantifier-free part strengthens this result). As a second result we show that anyalgorithm solving the problem has to ask at least about n2(namely Ω(n2/log n)) queries to the function, even when the expressionconsists of one μ and one ν (the assumption about thequantifier-free part weakens this result).

Most of the constructions of infinite words having polynomial subword complexity are quite complicated, e.g., sequences of Toeplitz, sequences defined by billiards in the cube, etc. In this paper, we describe a simple method for constructing infinite words w over a binary alphabet  { a,b }  with polynomial subword complexity pw. Assuming w contains an infinite number of a’s, our method is based on the gap function which gives the distances between consecutive b’s. It is known that if the gap function is injective, we can obtain at most quadratic subword complexity, and if the gap function is blockwise injective, we can obtain at most cubic subword complexity. Here, we construct infinite binary words w such that pw(n) = Θ(nβ) for any real number β > 1.

We study iteration and recursion operators in the denotational semantics of typedλ-calculi derived from the multiset relational model of linear logic.Although these operators are defined as fixpoints of typed functionals, we prove themfinitary in the sense of Ehrhard’s finiteness spaces.

In this paper we prove the decidability of the HD0L ultimate periodicity problem.