Digitala Vetenskapliga Arkivet

Endre søk
Begrens søket
12 1 - 50 of 83
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Treff pr side
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
Merk
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Holik, Lukag
    Vojnar, Tomas
    Mediating for reduction (on minimizing alternating Buchi automata)2014Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 552, s. 26-43Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We propose a new approach for minimizing alternating Buchi automata (ABA). The approach is based on the mediated equivalence on states of an ABA, which is the maximal equivalence contained in the mediated preorder. Two states p and q are related by the mediated preorder if there is a mediator (mediating state) which forward simulates p and backward simulates q. Under further conditions, letting a computation on some word jump from q to p preserves the language as the automaton can anyway already accept the word without jumps by runs through the mediator. We further show how the mediated equivalence can be computed efficiently. Finally, we show that, compared to the standard forward simulation equivalence, the mediated equivalence can yield much larger reductions when applied within the process of complementing Buchi automata where ABA are used as an intermediate model.

  • 2.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Univ Genoa, I-16126 Genoa, Italy..
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala Univ, Uppsala, Sweden..
    Sangnier, Arnaud
    Univ Paris Diderot, CNRS, LIAFA, Paris, France..
    Traverso, Riccardo
    FBK, Trento, Italy..
    Parameterized verification of time-sensitive models of ad hoc network protocols2016Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 612, s. 1-22Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.

  • 3.
    Aceto, Luca
    et al.
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101 Reykjavik, Iceland.
    Cimini, Matteo
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101 Reykjavik, Iceland.
    Ingolfsdottir, Anna
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101 Reykjavik, Iceland.
    Mousavi, Mohammad Reza
    Department of Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, Netherlands.
    Reniers, Michel A.
    Department of Mechanical Engineering, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, Netherlands.
    Rule Formats for Distributivity2012Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 458, s. 1-28Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats. Some conditions ensuring the invalidity of the left-distributivity law are also offered. © 2012 Elsevier B.V. All rights reserved.

  • 4.
    Aceto, Luca
    et al.
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101 Reykjavik, Iceland.
    Cimini, Matteo
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101 Reykjavik, Iceland.
    Ingolfsdottir, Anna
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101 Reykjavik, Iceland.
    Mousavi, Mohammad Reza
    Department of Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, Netherlands.
    Reniers, Michel A.
    Department of Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, Netherlands.
    SOS Rule Formats for Zero and Unit Elements2011Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 412, nr 28, s. 3045-3071Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain constants act as left or right unit/zero elements for a set of binary operators. Examples of left and right zero, as well as unit, elements from the literature are shown to fit the rule formats offered in this study. © 2011 Elsevier B.V. All rights reserved.

  • 5. Alimonti, P.
    et al.
    Kann, Viggo
    KTH, Tidigare Institutioner (före 2005), Numerisk analys och datalogi, NADA.
    Some APX-completeness results for cubic graphs2000Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 237, nr 2-Jan, s. 123-134Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Four fundamental graph problems, Minimum vertex cover, Maximum independent set, Minimum dominating set and Maximum cut, are shown to be APX-complete even for cubic graphs. Therefore, unless P = NP, these problems do not admit any polynomial time approximation scheme on input graphs of degree bounded by three.

  • 6. Aspvall, Bengt
    et al.
    Halldorsson, MM
    Manne, F
    Approximations for the general block distribution of a matrix2001Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 262, nr 1-2, s. 145-160Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The general block distribution of a matrix is a rectilinear partition of the matrix into orthogonal blocks such that the maximum sum of the elements within a single block is minimized. This corresponds to partitioning the matrix onto parallel processors so as to minimize processor load while maintaining regular communication patterns. Applications of the problem include various parallel sparse matrix computations, compilers for high-performance languages, particle in cell computations, video and image compression, and simulations associated with a communication network. We analyze the performance guarantee of a natural and practical heuristic based on iterative refinement, which has previously been shown to give good empirical results. When p2 is the number of blocks, we show that the tight performance ratio is Theta(rootp). When the matrix has rows of large cost, the details of the objective function of the algorithm are shown to be important, since a naive implementation can lead to a Ohm (p) performance ratio. Extensions to more general cost functions, higher-dimensional arrays, and randomized initial configurations are also considered. (C) 2001 Elsevier Science B.V. All rights reserved.

  • 7. Bar-Noy, Amotz
    et al.
    Cheilaris, Panagiotis
    Lampis, Michael
    Mitsou, Valia
    Zachos, Stathis
    Ordered Coloring for Grids and Related Graphs2011Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

     We investigate a coloring problem, called ordered coloring, in grids and some other families of grid-like graphs. Ordered coloring (also known as vertex ranking) is related to conflict-free coloring and other traditional coloring problems. Such coloring problems can model (among others) efficient frequency assignments in cellular networks. Our main technical results improve upper and lower bounds for the ordered chromatic number of grids and related graphs. To the best of our knowledge, this is the first attempt to calculate exactly the ordered chromatic number of these graph families.

  • 8. Bar-Noy, Amotz
    et al.
    Cheilaris, Panagiotis
    Lampis, Michael
    Graduate Center, City University of New York, 365 5th Avenue, New York, NY 10016, USA.
    Mitsou, Valia
    Zachos, Stathis
    Ordered coloring of grids and related graphs2012Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 444, s. 40-51Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We investigate a coloring problem, called ordered coloring, in grids and some other families of grid-like graphs. Ordered coloring (also known as vertex ranking) has applications, among other areas, in efficient solving of sparse linear systems of equations and scheduling parallel assembly of products. Our main technical results improve upper and lower bounds for the ordered chromatic number of grids and related graphs.

  • 9.
    Bender, Michael A.
    et al.
    SUNY Stony Brook, NY USA.
    Fekete, Sandor P.
    TU Braunschweig, Germany.
    Kroeller, Alexander
    TU Braunschweig, Germany.
    Liberatore, Vincenzo
    Case Western Reserve University, OH 44106 USA.
    Mitchell, Joseph S. B.
    SUNY Stony Brook, NY USA.
    Polishchuk, Valentin
    Linköpings universitet, Institutionen för teknik och naturvetenskap, Kommunikations- och transportsystem. Linköpings universitet, Tekniska fakulteten.
    Suomela, Jukka
    University of Helsinki, Finland; Aalto University, Finland.
    The minimum backlog problem2015Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 605, s. 51-61Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We study the minimum backlog problem (MBP). This online problem arises, e.g., in the context of sensor networks. We focus on two main variants of MBP. The discrete MBP is a 2-person game played on a graph G = (V, E). The player is initially located at a vertex of the graph. In each time step, the adversary pours a total of one unit of water into cups that are located on the vertices of the graph, arbitrarily distributing the water among the cups. The player then moves from her current vertex to an adjacent vertex and empties the cup at that vertex. The players objective is to minimize the backlog, i.e., the maximum amount of water in any cup at any time. The geometric MBP is a continuous-time version of the MBP: the cups are points in the two-dimensional plane, the adversary pours water continuously at a constant rate, and the player moves in the plane with unit speed. Again, the players objective is to minimize the backlog. We show that the competitive ratio of any algorithm for the MBP has a lower bound of Omega (D), where D is the diameter of the graph (for the discrete MBP) or the diameter of the point set (for the geometric MBP). Therefore we focus on determining a strategy for the player that guarantees a uniform upper bound on the absolute value of the backlog. For the absolute value of the backlog there is a trivial lower bound of Omega (D), and the deamortization analysis of Dietz and Sleator gives an upper bound of O (D log N) for N cups. Our main result is a tight upper bound for the geometric MBP: we show that there is a strategy for the player that guarantees a backlog of O(D), independently of the number of cups. We also study a localized version of the discrete MBP: the adversary has a location within the graph and must act locally (filling cups) with respect to his position, just as the player acts locally (emptying cups) with respect to her position. We prove that deciding the value of this game is PSPACE-hard. (C) 2015 Elsevier B.V. All rights reserved.

  • 10.
    Bengtsson, Fredrik
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Chen, Jingsen
    Ranking k maximum sums2007Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 377, nr 1-3, s. 229-237Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Given a sequence of n real numbers and an integer parameter k, the problem studied in this paper is to compute k subsequences of consecutive elements with the sums of their elements being the largest, the second largest, and the kth largest among all possible range sums of the input sequence. For any value of k, 1 <= k <= n (n + 1)/2, we design a fast algorithm that takes O (n + k log n) time in the worst case to compute and rank all such subsequences. We also prove that our algorithm is optimal for k = O (n) by providing a matching lower bound.Moreover, our algorithm is an improvement over the previous results on the maximum sum subsequences problem (where only the subsequences are requested and no ordering with respect to their relative sums will be determined).Furthermore, given the fact that we have computed the fth largest sums, our algorithm retrieves the (l + 1)th largest sum in O (log n) time, after O (n) time of preprocessing.

  • 11.
    Bensch, Suna
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Drewes, Frank
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Jürgensen, Helmut
    Department of Computer Science, Western University, London, Canada.
    van der Merwe, Brink
    Department of Computer Science, Stellenbosch University, South Africa.
    Graph transformation for incremental natural language analysis2014Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 531, s. 1-25Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Millstream systems have been proposed as a non-hierarchical method for modelling natural language. Millstream configurations represent and connect multiple structural aspects of sentences. We present a method by which the Millstream configurations corresponding to a sentence are constructed. The construction is incremental, that is, it proceeds as the sentence is being read and is complete when the end of the sentence is reached. It is based on graph transformations and a lexicon which associates words with graph transformation rules that implement the incremental construction process.

    Fulltekst (pdf)
    fulltext
  • 12.
    Berglund, Martin
    et al.
    Department of Information Science and Centre for AI Research, University of Stellenbosch, Matieland, South Africa.
    Bester, Willem
    Division of Computer Science, University of Stellenbosch, Matieland, South Africa.
    van der Merwe, Brink
    Division of Computer Science, University of Stellenbosch, Matieland, South Africa.
    Formalising and implementing Boost POSIX regular expression matching2021Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 857, s. 147-165Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Whereas Perl-compatible regular expression matchers typically exhibit some variation of leftmost-greedy semantics, those conforming to the posix standard are prescribed leftmost-longest semantics. However, the posix standard leaves some room for interpretation, and Fowler and Kuklewicz have done experimental work to confirm differences between various posix matchers. The Boost library has an interesting take on the posix standard, where it maximises the leftmost match not with respect to subexpressions of the regular expression pattern, but rather, with respect to capturing groups. In our work, we provide the first formalisation of Boost semantics, analyze the complexity of regular expression matching when using Boost semantics, and provide efficient algorithms for both online and multipass matching.

  • 13.
    Berglund, Martin
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Björklund, Henrik
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Björklund, Johanna
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Shuffled languages: representation and recognition2013Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 489-490, s. 1-20Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Language models that use interleaving, or shuffle, operators have applications in various areas of computer science, including system verification, plan recognition, and natural language processing. We study the complexity of the membership problem for such models, in other words, how difficult it is to determine if a string belongs to a language or not. In particular, we investigate how interleaving can be introduced into models that capture the context-free languages.

  • 14.
    Berglund, Martin
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    van der Merwe, Brink
    On the semantics of regular expression parsing in the wild2017Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 679, s. 69-82Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We introduce prioritized transducers to formalize capturing groups in regular expression matching in a way that permits straightforward modeling of capturing in Java's 1 regular expression library. The broader questions of parsing semantics and performance are also considered. In addition, the complexity of deciding equivalence of regular expressions with capturing groups is investigated.

  • 15.
    Berglund, Martin
    et al.
    Centre for AI Research, CSIR, Department of Information Science, Stellenbosch University, South Africa.
    van der Merwe, Brink
    Department of Computer Science, Stellenbosch University, South Africa.
    Re-examining regular expressions with backreferences2023Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 940, s. 66-80Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Most modern regular expression matching libraries (one of the rare exceptions being Google's RE2) allow backreferences, operations which bind a substring to a variable, allowing it to be matched again verbatim. However, both real-world implementations and definitions in the literature use different syntactic restrictions and have differences in the semantics of the matching of backreferences. Our aim is to compare these various flavors by considering the classes of formal languages that each can describe, establishing, as a result, a hierarchy of language classes. Beyond the hierarchy itself, some complexity results are given, and as part of the effort on comparing language classes new pumping lemmas are established, old classes are extended to new ones, and several incidental results on the nature of these language classes are given.

  • 16.
    Björklund, Henrik
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Björklund, Johanna
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Zechner, Niklas
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Compression of finite-state automata through failure transitions2014Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 557, s. 87-100Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Several linear-time algorithms for automata-based pattern matching rely on failure transitions for efficient back-tracking. Like epsilon transitions, failure transition do not consume input symbols, but unlike them, they may only be taken when no other transition is applicable. At a semantic level, this conveniently models catch-all clauses and allows for compact language representation.

    This work investigates the transition-reduction problem for deterministic finite-state automata (DFA). The input is a DFA A and an integer k. The question is whether k or more transitions can be saved by replacing regular transitions with failure transitions. We show that while the problem is NP-complete, there are approximation techniques and heuristics that mitigate the computational complexity. We conclude by demonstrating the computational difficulty of two related minimisation problems, thereby cancelling the ongoing search for efficient algorithms.

    Fulltekst (pdf)
    fulltext
  • 17.
    Björklund, Henrik
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Schwentick, Thomas
    On notions of regularity for data languages2010Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 411, nr 4-5, s. 702-715Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    With motivation from considerations in XML database theory and model checking, data strings have been introduced as an extension of finite alphabet strings which carry, at each position, a symbol and a data value from an infinite domain. Previous work has shown that it is difficult to come up with an expressive yet decidable automaton model for data languages. Recently, such a model, data automata, was introduced. This paper introduces a simpler but equivalent model and investigates its expressive power, algorithmic and closure properties, and some extensions.

  • 18.
    Björklund, Johanna
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Cohen, Shay B.
    University of Edinburgh, United Kingdom.
    Drewes, Frank
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Satta, Giorgio
    University of Padova, Italy.
    Bottom-up unranked tree-to-graph transducers for translation into semantic graphs2021Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 870, s. 3-28Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We develop a finite-state transducer for translating unranked trees into general graphs. This work is motivated by recent progress in semantic parsing for natural language, where sentences are first mapped into tree-shaped syntactic representations, and then these trees are translated into graph semantic representations. We investigate formal properties of our tree-to-graph transducers and develop a polynomial time algorithm for translating a weighted language of input trees into a packed representation, from which best-score graphs can be efficiently recovered.

    Fulltekst (pdf)
    fulltext
  • 19.
    Björklund, Johanna
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Drewes, Frank
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Jonsson, Anna
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Finding the N Best Vertices in an Infinite Weighted Hypergraph2017Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 682, s. 78s. 30-41Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We propose an algorithm for computing the N best vertices in a weighted acyclic hypergraph over a nice semiring. A semiring is nice if it is finitely-generated, idempotent, and has 1 as its minimal element. We then apply the algorithm to the problem of computing the N best trees with respect to a weighted tree automaton, and complement theoretical correctness and complexity arguments with experimental data. The algorithm has several practical applications in natural language processing, for example, to derive the N most likely parse trees with respect to a probabilistic context-free grammar. 

  • 20.
    Björklund, Johanna
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Öhman, Lars-Daniel
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för matematik och matematisk statistik.
    Simulation relations for pattern matching in directed graphs2013Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 485, s. 1-15Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We consider the problem of finding the occurrences of a pattern tree t in a directed graph g, and propose two algorithms, one for preprocessing and one for searching for t in g. It is assumed that the object graph itself is large and static, and that the pattern tree is small and frequently updated. To model varying abstraction levels in the data, we work with partially ordered alphabets and compute simulation relations rather than equivalence relations. In particular, vertices and edges are labelled with elements from a pair of preorders instead of unstructured alphabets. Under the above assumptions, we obtain a search algorithm that runs in time O(height (t) . vertical bar t vertical bar . vertical bar(V-g(+/-)t/R-g(+/-)t vertical bar(2)) where vertical bar (V-g(+/-)t/R-g(+/-)t)vertical bar is the number of equivalence classes in the coarsest simulation relation R-g(+/-)t on the graph g((+/-))t, the disjoint union of g and t. This means that the size of the object graph only affects the running time of the search algorithm indirectly, because of the groundwork done by the preprocessing routine in time O(k . vertical bar g vertical bar . vertical bar(V-g/R-g)vertical bar(2)), where vertical bar(V-g/R-g) is the number of equivalence classes in the coarsest simulation relation R-g on g, taking k = vertical bar V-g vertical bar(2) in the general case and k = height (g) if g is acyclic.

  • 21.
    Björner, Anders
    et al.
    KTH, Skolan för teknikvetenskap (SCI), Matematik (Inst.), Matematik (Avd.).
    Sagan, Bruce E.
    Rationality of the Mobius function of a composition poset2006Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 359, nr 3-Jan, s. 282-298Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We consider the zeta and Mobius functions of a partial order on integer compositions first studied by Bergeron, Bousquet-Melou, and Dulucq. The Mobius function of this poset was determined by Sagan and Vatter. We prove rationality of various formal power series in noncommuting variables whose coefficients are evaluations of the zeta function, zeta, and the Mobius function, mu. The proofs are either directly from the definitions or by constructing finite-state automata. We also obtain explicit expressions for generating functions obtained by specializing the variables to commutative ones. We reprove Sagan and Vatter's formula for it using this machinery. These results are closely related to those of Bjorner and Reutenauer about subword order, and we discuss a common generalization.

  • 22. Bryant, D.
    et al.
    Lagergren, Jens
    KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.
    Compatibility of unrooted phylogenetic trees is FPT2006Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 351, nr 3, s. 296-302Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    A collection of T-1, T-2,..., T-k of unrooted, leaf labelled (phylogenetic) trees, all with different leaf sets, is said to be compatible if there exists a tree T such that each tree T-i can be obtained from T by deleting leaves and contracting edges. Determining compatibility is NP-hard, and the fastest algorithm to date has worst case complexity of around Omega(n(k)) time, n being the number of leaves. Here, we present an O(nf (k)) algorithm, proving that compatibility of unrooted phylogenetic trees is fixed parameter tractable (FPT) with respect to the number k of trees.

  • 23.
    Böckenhauer, Hans-Joachim
    et al.
    ETH Zurich.
    Hromkovič, Juraj
    ETH Zurich.
    Královič, Richard
    ETH Zurich.
    Mömke, Tobias
    ETH Zurich.
    Rossmanith, Peter
    RWTH Aachen.
    Reoptimization of Steiner Trees: Changing the Terminal Set2009Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 410, nr 36, s. 3428-3435Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Given an instance of the Steiner tree problem together with an optimalsolution, we consider the scenario where this instance is modifiedlocally by adding one of the vertices to the terminal set or removing onevertex from it. In this paper, we investigate the problem whether theknowledge of an optimal solution to the unaltered instance can help insolving the locally modified instance. Our results are as follows:

    - We prove that these reoptimization variants of the Steiner treeproblem are NP-hard, even if edge costs are restricted to values from {1,2}.

    - We design 1.5-approximation algorithms for both variants of localmodifications. This is an improvement over the currently best knownapproximation algorithm for the classical Steiner tree problem whichachieves an approximation ratio of 1+ln(3)/2 \approx 1.55.

    - We present a PTAS for the subproblem in which the edge costs arenatural numbers {1,...,k} for some constant k.

    Fulltekst (pdf)
    fulltext
  • 24.
    Carlsson, Svante
    et al.
    Luleå tekniska universitet.
    Chen, Jingsen
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Mattsson, Christer
    Quality Laboratories AB, IDEON Research Park, Lund, Sweden.
    Heaps with bits1996Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 164, nr 1-2, s. 1-12Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We show how to improve the complexity of heap operations and heapsort using extra bits. We first study the parallel complexity of implementing priority queue operations on a heap. The tradeoff between the number of extra bits used, the number of processors available, and the parallel time complexity is derived. While inserting a new element into a heap in parallel can be done as fast as parallel searching in a sorted list, we show how to delete the smallest element from a heap in constant time with a sublinear number of processors, and in sublogarithmic time with a sublogarithmic number of processors. The models of parallel computation used are the CREW PRAM and the CRCW PRAM. Our results improve those of previously known algorithms. Moreover, we study a variant, the fine heap, of the traditional heap structure. A fast algorithm for constructing this new data structure is designed using an interesting technique, which is also used to develop an improved heapsort algorithm. Our variation of heapsort is faster than I. Wegener's (1993) heapsort and requires less extra space.

  • 25.
    Chiesa, Marco
    et al.
    Université catholique du Louvain, Belgium.
    Di Battista, G.
    Erlebach, T.
    Patrignani, M.
    Computational complexity of traffic hijacking under BGP and S-BGP2015Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 600, s. 143-154Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Harmful Internet hijacking incidents put in evidence how fragile interdomain routing is. In particular, the Border Gateway Protocol (BGP), which is used to exchange routing information between Internet entities, called Autonomous Systems (ASes), proved to be prone to attacks launched by a single malicious AS. Recent research contributions pointed out that even S-BGP, the secure variant of BGP that is being deployed, is not fully able to blunt traffic attraction attacks. Given a traffic flow between two ASes, we study how difficult it is for a malicious AS to devise a strategy for hijacking or intercepting that flow. The goal of the attack is to attract a traffic flow towards the malicious AS. While in the hijacking attack connectivity between the endpoints of a flow can be disrupted, in the interception attack connectivity must be maintained. We show that this problem marks a sharp difference between BGP and S-BGP. Namely, while it is solvable, under reasonable assumptions, in polynomial time for the type of attacks that are usually performed in BGP, it is NP-hard for S-BGP. Our study has several by-products. E.g., we solve a problem left open in the literature, stating when performing a hijacking in S-BGP is equivalent to performing an interception.

  • 26. Chilton, Chris
    et al.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kwiatkowska, Marta
    An algebraic theory of interface automata2014Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 549, s. 146-174Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We formulate a compositional specification theory for interface automata, where a component model specifies the allowed sequences of input and output interactions with the environment. A trace-based linear-time refinement is provided, which is the weakest preorder preserving substitutivity of components, and is weaker than the classical alternating simulation defined on interface automata. Since our refinement allows a component to be refined by refusing to produce any output, we also define a refinement relation that guarantees safety and progress. The theory includes the operations of parallel composition to support the structural composition of components, logical conjunction and disjunction for independent development, hiding to support abstraction of interfaces, and quotient for incremental synthesis of components. Our component formulation highlights the algebraic properties of the specification theory for both refinement preorders, and is shown to be fully abstract with respect to observation of communication mismatches. Examples of independent and incremental component development are provided.

  • 27.
    Coimbra, Danilo B.
    et al.
    Federal University of Bahia (UFBA), Brazil.
    Martins, Rafael Messias
    Linnéuniversitetet, Fakulteten för teknik (FTK), Institutionen för datavetenskap och medieteknik (DM).
    Mota, Edson
    Federal University of Bahia (UFBA), Brazil.
    Tiburtino, Tacito
    PAIVA – NCEx – Federal University of Alagoas (UFAL), Brazil.
    Diamantino, Pedro
    Federal University of Bahia (UFBA), Brazil.
    Peixoto, Maycon L. M.
    Federal University of Bahia (UFBA), Brazil;University of Campinas, Brazil.
    Analyzing the quality of local and global multidimensional projections using performance evaluation planning2021Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 872, s. 41-54Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Among the challenges of the big data era, the analysis of high-dimensional data is still an open research area. As a result, several multidimensional projection techniques have been developed to reduce data dimensionality, becoming important visualization and visual analytics tools. In order to ensure the quality of projections, it is necessary to assess the low-dimensional embeddings by using different dataset configurations as input and analyzing evaluation metrics. However, it is not clear to the user how factors such as the number of dimensions, instances, or clusters, can affect the projection mapping and its quality regarding different projection techniques and assessment metrics. The research reported in this paper aims to clarify how much these factors affect each response variable via performance evaluation planning. We present an evaluation approach, supported by factorial design, that carries out a complete analysis, in the sense of measuring all possible combinations of all the input factors. The results of the analyses of local and global structure preservation in the projections yield a better understanding of how distinct dataset properties can influence the choice of projections based on quality metrics results. (C) 2021 Elsevier B.V. All rights reserved.

  • 28.
    Dahllöf, Vilhelm
    et al.
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, TCSLAB - Laboratoriet för teoretisk datalogi.
    Jonsson, Peter
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, TCSLAB - Laboratoriet för teoretisk datalogi.
    Beigel, R.
    Department of Computer Science, Temple University, 1805 N Broad St Fl 4, Philadelphia, PA 19122, United States.
    Algorithms for four variants of the exact satisfiability problem2004Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 320, nr 2-3, s. 373-394Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present four polynomial space and exponential time algorithms for variants of the EXACT SATISFIABILITY problem. First, an O(1.1120n) (where n is the number of variables) time algorithm for the NP-complete decision problem of EXACT 3-SATISFIABILITY, and then an O(1.1907n) time algorithm for the general decision problem of EXACT SATISFIABILITY. The best previous algorithms run in O(1.1193n) and O(1.2299n) time, respectively. For the #P-complete problem of counting the number of models for EXACT 3-SATISFIABILITY we present an O(1.1487n) time algorithm. We also present an O(1.2190n) time algorithm for the general problem of counting the number of models for EXACT SATISFIABILITY, presenting a simple reduction, we show how this algorithm can be used for computing the permanent of a 0/1 matrix. © 2004 Elsevier B.V. All rights reserved.

  • 29.
    Dalmau, Victor
    et al.
    Departament de Tecnologia Universitat Pompeu Fabra.
    Jonsson, Peter
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, TCSLAB - Laboratoriet för teoretisk datalogi.
    The Complexity of Counting Homomorphisms Seen from the Other Side2004Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 329, s. 315-323Artikkel i tidsskrift (Fagfellevurdert)
  • 30.
    Drewes, Frank
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Preface2017Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 679, s. 1-1Artikkel i tidsskrift (Annet vitenskapelig)
  • 31.
    Drewes, Frank
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Janssens, Dirk
    University of Antwerp.
    Hoffmann, Berthold
    University of Bremen.
    Minas, Mark
    University of the German Armed Forces Munich.
    Adaptive Star grammars and their languages2010Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 411, nr 34-36, s. 3090-3109Artikkel i tidsskrift (Fagfellevurdert)
  • 32.
    Drewes, Frank
    et al.
    Umeå universitet, Teknisk-naturvetenskapliga fakulteten, Institutionen för datavetenskap.
    Mörbitz, Richard
    Technische Universität Dresden, Germany.
    Vogler, Heiko
    Technische Universität Dresden, Germany.
    Hybrid tree automata and the yield theorem for constituent tree automata2023Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 979, artikkel-id 114185Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We introduce an automaton model for recognizing sets of hybrid trees, the hybrid tree automaton (HTA). Special cases of hybrid trees are constituent trees and dependency trees, as they occur in natural language processing. This includes the cases of discontinuous constituent trees and non-projective dependency trees. In general, a hybrid tree is a tree over a ranked alphabet in which a symbol can additionally be equipped with a natural number, called index; in a hybrid tree, each index occurs at most once. The yield of a hybrid tree is a sequence of strings over those symbols which occur in an indexed form; the corresponding indices determine the order within these strings; the borders between two consecutive strings are determined by the gaps in the sequence of indices. As a special case of HTA, we define constituent tree automata (CTA) which recognize sets of constituent trees. We introduce the notion of CTA-inductively recognizable and we show that the set of yields of a CTA-inductively recognizable set of constituent trees is an LCFRS language, and vice versa.

  • 33.
    El Ouali, Mourad
    et al.
    University of Kiel, Germany.
    Fohlin, Helena
    Linköpings universitet, Institutionen för klinisk och experimentell medicin, Avdelningen för kliniska vetenskaper. Linköpings universitet, Hälsouniversitetet. Östergötlands Läns Landsting, Centrum för hälso- och vårdutveckling, Regionalt cancercentrum.
    Srivastav, Anand
    University of Kiel, Germany.
    A randomised approximation algorithm for the hitting set problem2014Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 555, s. 23-34Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Let H = (V, epsilon) be a hypergraph with vertex set V and edge set epsilon, where n := vertical bar V vertical bar and m := vertical bar epsilon vertical bar. Let l be the maximum size of an edge and Delta be the maximum vertex degree. A hitting set (or vertex cover) in H is a subset of V in which all edges are incident. The hitting set problem is to find a hitting set of minimum cardinality. It is known that an approximation ratio of l can be achieved easily. On the other hand, for constant l, an approximation ratio better than l cannot be achieved in polynomial time under the unique games conjecture (Khot and Regev, 2008 [17]). Thus breaking the l-barrier for significant classes of hypergraphs is a complexity-theoretically and algorithmically interesting problem, which has been studied by several authors (Krivelevich, 1997 [18], Halperin, 2000 [12], Okun, 2005 [23]). We propose a randomised algorithm of hybrid type for the hitting set problem, which combines LP-based randomised rounding, graphs sparsening and greedy repairing and analyse it for different classes of hypergraphs. For hypergraphs with Delta = O(n1/4) and l = O (root n) we achieve an approximation ratio of l(1 - c/Delta), for some constant c greater than 0, with constant probability. For the case of hypergraphs where l and Delta are constants, we prove a ratio of l(1 - l-1/8 Delta). The latter is done by analysing the expected size of the hitting set and using concentration inequalities. Moreover, for quasi-regularisable hypergraphs, we achieve an approximation ratio of l(1 - n/8m). We show how and when our results improve over the results of Krivelevich, Halperin and Okun.

  • 34.
    Elias, Isaac
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.
    Lagergren, Jens
    KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.
    Fast Neighbor Joining2009Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 410, nr 21-23, s. 1993-2000Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

     Reconstructing the evolutionary history of a set of species is a fundamental problem in biology and methods for solving this problem are gaged based on two characteristics: accuracy and efficiency. Neighbor joining (NJ) is a so-called distance-based method that, thanks to its good accuracy and speed, has been embraced by the phylogeny community. it takes the distances between n taxa and produces in Theta(n(3)) time a phylogenetic tree, i.e., a tree which aims to describe the evolutionary history of the taxa. In addition to performing well in practice, the NJ algorithm has optimal reconstruction radius.

    The contribution of this paper is twofold: (1) we present an algorithm called Fast Neighbor Joining(FNJ) with optimal reconstruction radius and optimal run time complexity O(n(2)) and (2) we present a greatly simplified proof for the correctness of NJ. initial experiments show that FNJ in practice has almost the same accuracy as NJ, indicating that the property of optimal reconstruction radius has great importance to their good performance. Moreover, we show how improved running time can be achieved for Computing the so-called correction formulas.

  • 35.
    Engebretsen, Lars
    et al.
    KTH, Tidigare Institutioner (före 2005), Numerisk analys och datalogi, NADA.
    Holmerin, Jonas
    KTH, Tidigare Institutioner (före 2005), Numerisk analys och datalogi, NADA.
    Russell, A.
    Inapproximability results for equations over finite groups2004Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 312, nr 1, s. 17-45Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    An equation over a finite group G is an expression of form w(1)w(2). . .w(k) = 1(G), where each w(i) is a variable, an inverted variable, or a constant from G; such an equation is satisfiable if there is a setting of the variables to values in G so that the equality is realized. We study the problem of simultaneously satisfying a family of equations over a finite group G and show that it is NP-hard to approximate the number of simultaneously satisfiable equations to within \G\ - epsilon for any epsilon > 0. This generalizes results of Hastad (J. ACM 48 (4) (2001) 798), who established similar bounds under the added condition that the group G is Abelian.

  • 36.
    Eriksen, Niklas
    Dept. of Mathematics, Royal Institute of Technology, Stockholm.
    (1+eps)-approximation of sorting by reversals and transpositions2002Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 289, nr 1, s. 517-529Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Gu et al. gave a 2-approximation for computing the minimal number of inversions and transpositions needed to sort a permutation. There is evidence that, from the point of view of computational molecular biology, a more adequate objective function is obtained, if transpositions are given double weight. We present a (1+eps)-approximation for this problem, based on the exact algorithm of Hannenhalli and Pevzner, for sorting by reversals only.

    Fulltekst (pdf)
    fulltext
  • 37.
    Eriksen, Niklas
    Mathematical Sciences, Göteborg University and Chalmers University of Technology, Göteborg.
    Reversal and Transposition Medians2007Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 374, nr 1-3, s. 111-126Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In determining phylogenetic trees using gene order information, medians provide a powerful alternative to pairwise distances. On the other hand, both breakpoint and reversal medians are NP-hard to compute and the use of medians has been limited to relatively closely related genomes. In this paper, we show that in spite of the greater non-uniqueness of reversal medians, compared to breakpoint medians, medians of moderately distant genomes are often widely spread. This means that regardless of which approximation algorithms one may device for computing reversal medians, the genomes need to be closely related for phylogenetic tree computations to be successful. To show this, we use results on transposition medians, which behave similarly, and also support our claims with simulations and a real data example with widely spread medians.

  • 38.
    Fersman, Elena
    et al.
    Uppsala University, Sweden.
    Mokrushin, Leonid
    Uppsala University, Sweden.
    Pettersson, Paul
    Uppsala University, Sweden.
    Yi, Wang
    Uppsala University, Sweden.
    Schedulability Analysis of Fixed Priority Systems using Timed Automata2006Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 354, nr 2, s. 301-317Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In classic scheduling theory, real-time tasks are usually assumed to be periodic, i.e. tasks are released and computed with fixed rates periodically. To relax the stringent constraints on task arrival times, we propose to use timed automata to describe task arrival patterns. In a previous work, it is shown that the general schedulability checking problem for such models is a reachability problem for a decidable class of timed automata extended with subtraction. Unfortunately, the number of clocks needed in the analysis is proportional to the maximal number of schedulable task instances associated with a model, which is in many cases huge. In this paper, we show that for fixed-priority scheduling strategy, the schedulability checking problem can be solved using standard timed automata with two extra clocks in addition to the clocks used in the original model to describe task arrival times. The analysis can be done in a similar manner to response time analysis in classic Rate-Monotonic Analysis (RMA). The result is further extended to systems with data-dependent control, in which the release time of a task may depend on the time-point at which other tasks finish their execution. For the case when the execution times of tasks are constants, we show that the schedulability problem can be solved using n+1 extra clocks, where n is the number of tasks. The presented analysis techniques have been implemented in the Times tool. For systems with only periodic tasks, the performance of the tool is comparable with tools implementing the classic RMA technique based on equation-solving, without suffering from the exponential explosion in the number of tasks.

  • 39.
    Fersman, Elena
    et al.
    Ericsson Research, Ericsson AB.
    Mokrushin, Leonid
    Pettersson, Paul
    Yi, Wang
    Schedulability Analysis of Fixed-Priority Systems using Timed Automata2006Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 354, nr 2, s. 301-317Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In classic scheduling theory, real-time tasks are usually assumed to be periodic, i.e. tasks are released and computed with fixed rates periodically. To relax the stringent constraints on task arrival times, we propose to use timed automata to describe task arrival patterns. In a previous work, it is shown that the general schedulability checking problem for such models is a reachability problem for a decidable class of timed automata extended with subtraction. Unfortunately, the number of clocks needed in the analysis is proportional to the maximal number of schedulable task instances associated with a model, which is in many cases huge. In this paper, we show that for fixed-priority scheduling strategy, the schedulability checking problem can be solved using standard timed automata with two   extra clocks in addition to the clocks used in the original model to describe task arrival times. The analysis can be done in a similar manner to response time analysis in classic Rate-Monotonic Analysis (RMA). The result is further extended to systems with data-dependent control, in which the release time of a task may depend on the time-point at which other tasks finish their execution. For the case when the execution times of tasks are constants, we show that the schedulability problem can be solved using n+1n+1 extra clocks, where nn is the number of tasks. The presented analysis techniques have been implemented in the Times tool. For systems with only periodic tasks, the performance of the tool is comparable with tools implementing the classic RMA technique based on equation-solving, without suffering from the exponential explosion in the number of tasks.

  • 40.
    Freivalds, R.
    et al.
    Latvian State Univ.
    Bonner, Richard
    Mälardalens högskola, Institutionen för matematik och fysik.
    Quantum inductive inference by finite automata2008Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 397, nr 1-3, s. 70-76Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Freivalds and Smith [R. Freivalds, C.H. Smith Memory limited inductive inference machines, Springer Lecture Notes in Computer Science 621 (1992) 19-29] proved that probabilistic limited memory inductive inference machines can learn with probability 1 certain classes of total recursive functions, which cannot be learned by deterministic limited memory inductive inference machines. We introduce quantum limited memory inductive inference machines as quantum finite automata acting as inductive inference machines. These machines, we show, can learn classes of total recursive functions not learnable by any deterministic, nor even by probabilistic, limited memory inductive inference machines.

  • 41. Fried, D.
    et al.
    Shimony, S. E.
    Benbassat, A.
    Wenner, Cenny
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Complexity of Canadian traveler problem variants2013Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 487, s. 1-16Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The Canadian traveler problem (CTP) is the problem of traversing a given graph, where some of the edges may be blocked-a state which is revealed only upon reaching an incident vertex. Originally stated by Papadimitriou and Yannakakis (1991) [1], the adversarial version of the CTP was shown to be PSPACE-complete, with the stochastic version shown to be in PSPACE and #P-hard. We show that the stochastic CTP is also PSPACE-complete: initially proving PSPACE-hardness for the dependent version of the stochastic CTP, and proceeding with gadgets that allow us to extend the proof to the independent case. Since for disjoint-path graphs, the CTP can be solved in polynomial time, we examine the complexity of the more general remote-sensing CTP, and show that it is NP-hard even for disjoint-path graphs.

  • 42. Fried, Dror
    et al.
    Shimony, Solomon Eyal
    Benbassat, Amit
    Wenner, Cenny
    Stockholms universitet, Naturvetenskapliga fakulteten, Numerisk analys och datalogi (NADA). KTH Royal Inst Technol, SE-10044 Stockholm, Sweden.
    Complexity of Canadian traveler problem variants2013Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 487, s. 1-16Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The Canadian traveler problem (CTP) is the problem of traversing a given graph, where some of the edges may be blocked a state which is revealed only upon reaching an incident vertex. Originally stated by Papadimitriou and Yannakakis (1991) [1], the adversarial version of the CTP was shown to be PSPACE-complete, with the stochastic version shown to be in PSPACE and #P-hard. We show that the stochastic CTP is also PSPACE-complete: initially proving PSPACE-hardness for the dependent version of the stochastic CTP, and proceeding with gadgets that allow us to extend the proof to the independent case. Since for disjoint-path graphs, the CTP can be solved in polynomial time, we examine the complexity of the more general remote-sensing CTP, and show that it is NP-hard even for disjoint-path graphs.

  • 43. Gambino, Nicola
    et al.
    Garner, Richard
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Matematiska institutionen.
    The identity type weak factorisation system2008Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 409, nr 1, s. 94-109Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We show that the classifying category C(T) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.

  • 44.
    Glasser, Christian
    et al.
    Julius Maximilian University, Germany.
    Jonsson, Peter
    Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten.
    Martin, Barnaby
    University of Durham, England.
    Circuit satisfiability and constraint satisfaction around Skolem Arithmetic2017Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 703, s. 18-36Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We study interactions between Skolem Arithmetic and certain classes of Circuit Satisfiability and Constraint Satisfaction Problems (CSPs). We revisit results of Glasser et al. [1] in the context of CSPs and settle the major open question from that paper, finding a certain satisfiability problem on circuits-involving complement, intersection, union and multiplication-to be decidable. This we prove using the decidability of Skolem Arithmetic. Then we solve a second question left open in [1] by proving a tight upper bound for the similar circuit satisfiability problem involving just intersection, union and multiplication. We continue by studying first-order expansions of Skolem Arithmetic without constants, (N; x), as CSPs. We find already here a rich landscape of problems with non-trivial instances that are in P as well as those that are NP-complete. (C) 2017 Elsevier B.V. All rights reserved.

  • 45.
    Goranko, Valentin
    et al.
    Stockholms universitet, Humanistiska fakulteten, Filosofiska institutionen. University of Johannesburg, South Africa.
    Kuusisto, Antti
    Rönnholm, Raine
    Alternating-time temporal logic ATL with finitely bounded semantics2019Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 797, s. 129-155Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We study a variant ATL(FB) of the alternating-time temporal logic ATL with a nonstandard, 'finitely bounded' semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL(FB) differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL(FB). The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL(FB) and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL(FB) and prove its soundness and completeness. 

  • 46.
    Grinchtein, Olga
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Leucker, Martin
    Learning of event-recording automata2010Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 411, nr 47, s. 4029-4054Artikkel i tidsskrift (Fagfellevurdert)
  • 47.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente, Netherlands .
    Reducing behavioural to structural properties of programs with procedures2013Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 480, s. 69-103Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. The present paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with procedures, abstracting away completely from program data, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. In addition, we show how the translation can be extended beyond the basic flow graph model and safety logic to richer behavioural models (such as open programs) and richer program models (including Boolean programs), and discuss possible extensions for more complex logics. We present several applications of the characterisation, in particular sound and complete compositional verification for behavioural properties based on maximal models.

  • 48.
    Haller, Philipp
    et al.
    EPFL, Switzerland.
    Odersky, Martin
    EPFL, Switzerland.
    Scala Actors: Unifying thread-based and event-based programming2009Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 410, nr 2-3, s. 202-220Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    There is an impedance mismatch between message-passing concurrency and virtual machines, such as the JVM. VMs usually map their threads to heavyweight OS processes. Without a lightweight process abstraction, users are often forced to write parts of concurrent applications in an event-driven style which obscures control flow, and increases the burden on the programmer. In this paper we show how thread-based and event-based programming can be unified under a single actor abstraction. Using advanced abstraction mechanisms of the Scala programming language, we implement our approach on unmodified JVMs. Our programming model integrates well with the threading model of the underlying VM.

  • 49. Hammar, Mikael
    et al.
    Nilsson, Bengt J
    Malmö högskola, Teknik och samhälle (TS).
    Persson, Mia
    Malmö högskola, Teknik och samhälle (TS).
    Competitive Exploration of Rectilinear Polygons2006Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 354, nr 3, s. 367-378Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Exploring a polygon with robots, when the robots do not have knowledge of the surroundings can be viewed as an online problem. Typical for online problems is that decisions must be made based on past events without complete information about the future. In our case the robots do not have complete information about the environment. Competitive analysis can be used to measure the performance of methods solving online problems. The competitive ratio of such a method is the ratio between the method's performance and the performance of the best method having full knowledge of the future. We are interested in obtaining good bounds on the competitive ratio of exploring polygons and prove constant competitive strategies and lower bounds for exploring a simple rectilinear polygon in the $L_1$ metric.

    Fulltekst (pdf)
    FULLTEXT01
  • 50.
    Hamrin, Göran
    et al.
    Matematiska institutionen, Uppsala universitet.
    Stoltenberg-Hansen, Viggo
    Matematiska institutionen, Uppsala universitet.
    Two categories of effective continuous cpos2006Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 365, nr 3, s. 216-236Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    This paper presents two categories of effective continuous complete partial orders (cpos). We define a new criterion on the basis of a cpo so as to make the resulting category of consistently complete continuous cpos cartesian closed. We also generalise to continuous cpos the definition of a complete set, which was used as a definition of effective bifinite domains in Hamrin and Stoltenberg-Hansen [Cartesian closed categories of effective domains, in: H. Schwichtenberg, R. Steinbruggen (Eds.), Proof and System-Reliability, Kluwer Academic Publishers, Dordrecht, 2002, pp. 1-20], and investigate the closure results that can be obtained.

12 1 - 50 of 83
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf