waashk/dblp huggingface dataset:
guarded fixed point logics and the monadic theory of countable trees. different variants of guarded logics (a powerful generalization of modal logics) are surveyed and an elementary proof for the decidability of guarded fixed point logics is presented. in a joint paper with igor walukiewicz, we proved that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time (e. grädel and i. walulkiewicz, proc. 14th ieee symp. on logic in computer science, 1999, pp. 45-54). that proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. the exposition given here emphasizes the tree model property of guarded logics: every satisfiable sentence has a model of bounded tree width. based on the tree model property, we show that the satisfiability problem for guarded fixed point formulae can be reduced to the monadic theory of countable trees (sωs), or to the µ-calculus with backwards modalities.
on maximal codes with a finite interpreting delay. the notion of codes with a finite interpreting delay (f.i.d.) was introduced in (guesnet, theoret. inform. appl. 34 (2000) 47-59). in this paper, we are interested in the notion of maximality for f.i.d. codes. we characterize the maximal f.i.d. codes in terms of completeness. we also present an embedding procedure keeping thinness, rationality and the delay.
on maximal synchronous codes. in this paper, we are interested in maximal synchronous codes. more precisely, we prove that we can embed any synchronous code in a maximal one. moreover, we establish that, for synchronous codes, the notion of maximality in the family of synchronous codes is equivalent to the notion of maximality in the family of codes.
on temporal logic versus datalog. we provide a direct and modular translation from the temporal logics ctl, etl, fctl (ctl extended with the ability to express fairness) and the modal µ-calculus to monadic inf-datalog with built-in predicates. we call it inf-datalog because the semantics we provide is a little different from the conventional datalog least fixed point semantics, in that some recursive rules (corresponding to least fixed points) are allowed to unfold only finitely many times, whereas others (corresponding to greatest fixed points) are allowed to unfold infinitely many times.we characterize the fragments of monadic inf-datalog that have the same expressive power as modal logic (resp. ctl, alternation-free modal µ-calculus and modal µ-calculus). our translation is interesting because it is direct and succinct. moreover the fragments of monadic inf-datalog that we have exhibited have very simple syntactic characterizations as subsets of what we call modal inf-datalog programs.
algebraic rewritings for optimizing regular path queries. rewriting queries using views is a powerful technique that has applications in query optimization, data integration, data warehousing, etc. query rewriting in relational databases is by now rather well investigated. however, in the framework of semistructured data the problem of rewriting has received much less attention. in this paper we focus on extracting as much information as possible from algebraic rewritings for the purpose of optimizing regular path queries. the cases when we can find a complete exact rewriting of a query using a set a views are very "ideal". however, there is always information available in the views, even if this information is only partial. we introduce "lower" and "possibility" partial rewritings and provide algorithms for computing them. these rewritings are algebraic in their nature, i.e. we use only the algebraic view definitions for computing the rewritings. we do not use any pairs (tuples) of objects for computing the rewritings. this fact makes them a main memory product, which can be used for reducing secondary memory and remote access. after the main memory algebraic computation of the rewritings there is a second phase, with secondary memory access, for deriving the pairs of objects in the query answer. we give two algorithms for utilizing the partial lower and partial possibility rewritings to decrease the number of secondary memory accesses.
sorted dependency insertion grammars. an enhanced generative formalism is proposed based on the combination of two features: contextual derivation (as in marcus contextual grammars) and sorted dependency structures (as in dependency grammars). the model is related to a variant of restarting automaton with rewriting and deletion. preliminary results on the generative power as well as closure and decidability properties of the new model are presented.
acyclic networks maximizing the printing complexity. this article estimates the worst-case running time complexity for traversing and printing all successful paths of a normalized trim acyclic automaton. first, we show that the worst-case structure is a festoon. then, we prove that the complexity is maximal when we have a distribution of e (napier constant) outgoing arcs per state on average, and that it can be exponential in the number of arcs.
two polygraphic presentations of petri nets. this document gives an algebraic and two polygraphic translations of petri nets, all three providing an easier way to describe reductions and to identify some of them. the first one sees places as generators of a commutative monoid and transitions as rewriting rules on it: this setting is totally equivalent to petri nets, but lacks any graphical intuition. the second one considers places as one-dimensional cells and transitions as two-dimensional ones: this translation recovers a graphical meaning but raises many diffficulties since it uses explicit permutations. finally, the third translation sees places as degenerated two-dimensional cells and transitions as three-dimensional ones: this is a setting equivalent to petri nets, equipped with a graphical interpretation.
distributivity of categories of coalgebras. for any set-endofunctor f, the category setf of f-coalgebras has preimages, i.e. pullbacks along an injective map. if f preserves preimages, then setf is distributive, and the converse holds, whenever setf has finite products.
a spatial view of information. spatial representation has two contrasting but interacting aspects (i) representation of spaces and (ii) representation by spaces. in this paper we will examine two aspects that are common to both interpretations of the theme of spatial representation, namely nerve-type constructions and refinement. we consider the induced structures, in which some of the attributes of the informational context are sampled.
on a modular domination game. we present a generalization of the so-called σ-game, introduced by sutner (math. intelligencer 11 (1989) 49), a combinatorial game played on a graph, with relations to cellular automata, as well as odd domination in graphs. a configuration on a graph is an assignment of values in {0,...,p- 1} (where p is an arbitrary positive integer) to all the vertices of g. one may think of a vertex v of g as a button the player can press at his discretion. if vertex v is chosen, the value of all the vertices adjacent to v increases by 1 modulo p. this defines an equivalence relation between the configurations: two configurations are in relation if it is possible to reach one from the other by a sequence of such operations. we investigate the number of equivalence classes that a given graph has, and we give formulas for trees and special regular graphs.
truly concurrent constraint programming. we study "causality" relationships in concurrent constraint programming: what is observed is not just the conjunction of constraints deposited in the store, but also the causal dependencies between these constraints. we describe a denotational semantics for cc that is fully abstract with respect to observing this "causality" relation on constraints. this semantics preserves more fine-grained structure of computation; in particular the interleaving law is not verified ( is indeterminate choice). relationships between such a denotational approach to true concurrency and different powerdomain constructions are explored.
semantic essence of asml. the abstract state machine language, asml, is a novel executable specification language based on the theory of abstract state machines. asml is object-oriented, provides high-level mathematical data-structures, and is built around the notion of synchronous updates and finite choice. asml is fully integrated into the .net framework and microsoft development tools. in this paper, we explain the design rationale of asml and provide static and dynamic semantics for a kernel of the language.
partial updates. a datastructure instance, e.g. a set or file or record, may be modified independently by different parts of a computer system. the modifications may be nested. such hierarchies of modifications need to be efficiently checked for consistency and integrated. this is the problem of partial updates in a nutshell. in our first paper on the subject, we developed an algebraic framework which allowed us to solve the partial update problem for some useful datastructures including counters, sets and maps. these solutions are used for the efficient implementation of concurrent data modifications in the specification language asml. the two main contributions of this paper are (i) a more general algebraic framework for partial updates and (ii) a solution of the partial update problem for sequences and labeled ordered trees.
modelization of deterministic rational relations. the definition of the class of deterministic rational relations is fundamentally based on the read-only one-way turing machine approach. the notion of deterministic automata developed up to now is too strong and asks for an unnatural detour via end-markers to give all deterministic rational relations (cf. section 3.1). we stress that several conditions usually considered as related to determinism are mere normalizations of determinism and are not inherent to the notion (cf. section 3.2). in this paper, we introduce pertinent notions of deterministic labelled graph automata (cf. section 3.3) which avoid any use of end-markers: strong deterministic, n-deterministic automata for nn. these notions form an increasing infinite hierarchy of classes of automata which all lead to the same usual class of deterministic rational relations. moreover, the class corresponding to the natural extension to the case n= is exactly the class of unambiguous automata. we also consider nivat's characterization via multimorphisms applied to rational languages and introduce a hierarchy of deterministic versions of multimorphisms. properties of determinism and unambiguity are compared. the decision problems for ambiguity or determinism relative to automata and multimorphisms are settled. roughly, all problems are undecidable in case of arity 2 with at least two non-binary alphabets, else they are decidable, most being even polynomial time decidable.
on the relationship between nlc-width and linear nlc-width. in this paper, we consider nlc-width, nlct-width, and linear nlc-width bounded graphs. we show that the set of all complete binary trees has unbounded linear nlc-width and that the set of all co-graphs has unbounded nlct-width. since trees have nlct-width 3 and co-graphs have nlc-width 1, it follows that the family of linear nlc-width bounded graph classes is a proper subfamily of the family of nlct-width bounded graph classes and that the family of nlct-width bounded graph classes is a proper subfamily of the family of nlc-width bounded graph classes.
vertex disjoint paths on clique-width bounded graphs. we show that the l vertex disjoint paths problem between l pairs of vertices can be solved in linear time for co-graphs but is np-complete for graphs of clique-width at most 6 and nlc-width at most 4. the np-completeness follows from the fact that the line graph of a graph of tree-width k has clique-width at most 2k + 2 and nlc-width at most k + 2, and a result by nishizeki et al. [the edge-disjoint paths problem is np-complete for series-parallel graphs, discrete appl. math. 115 (2001) 177-186]. the vertex disjoint paths problem is the first graph problem shown to be np-complete on graphs of bounded clique-width but solvable in linear time on co-graphs and graphs of bounded tree-width. additionally, we show that the r vertex disjoint paths problem between each of l pairs of vertices can be solved in polynomial time for co-graphs, if l is given to the input, and for graphs of bounded clique-width, if l is fixed.
kolmogorov complexity and non-determinism. we are concerned with kolmogorov complexity of strings produced by non-deterministic algorithms. for this, we consider five classes of non-deterministic description modes: (i) non-bounded description modes in which the number of outputs depends on programs, (ii) distributed description modes in which the number of outputs depends on the size of the outputs, (iii) spread description modes in which the number of outputs depends on both programs and the size of the outputs, (iv) description modes for which each string has a unique minimal description, and lastly (v) description modes for which the set of minimal length descriptions is a prefix set.
a note on a scale-sensitive dimension of linear bounded functionals in banach spaces. we show that "b is of type p > 1" is a necessary and sufficient condition for a learnability of a class of linear bounded functionals with norm < 1 restricted to the unit ball in banach space b. on the way, we give very short probabilistic proof for vapnik's result (hilbert space and improved) and improve our result with pascal koiran for convex halls of indicator functions. the approach we use in this paper allows to connect various results about learnability and approximation.
metaphors and heuristic-driven theory projection (hdtp). a classical approach of modeling metaphoric expressions uses a source concept network that is mapped to a target concept network. both networks are often represented as algebras. in this paper, a representation using the mathematically sound framework of heuristic-driven theory projection (hdtp) is presented which is--although quite different from classical approaches--algebraic in nature, too. hdtp has the advantage that a structural description of source and target can be given and the connection between both domains are more clearly specified. the major aspects of the formal properties of hdtp, the specification of the underlying algorithm hdtp-a, and the development of a formal semantics for analogical reasoning will be discussed. we will apply hdtp to different types of metaphors.
equations in free semigroups with involution and their relation to equations in free groups. a free semigroup with involution (fsi) is essentially the set of words over a given alphabet plus an operator which reverses words. the paper introduces equations in fsi and show that they are the right objects to deal with when studying the complexity of equations in free groups. on these lines, we generalize to fsi several results valid for word equations, like the overlapping lemma, the 2o(|e|)-bound on the exponent of periodicity of minimal solutions, and the np-hard lower bound.the main result of the paper is the reduction of the problem of satisfiability of equations in free groups to the satisfiability of equations in fsi by a non-deterministic polynomial time transformation.
algebraic proof systems over formulas. we introduce two algebraic propositional proof systems f-ns and f-pc. the main difference of our systems from (customary) nullstellensatz and polynomial calculus is that the polynomials are represented as arbitrary formulas (rather than sums of monomials). short proofs of tseitin's tautologies in the constant-depth version of f-ns provide an exponential separation between this system and polynomial calculus.we prove that f-ns (and hence f-pc) polynomially simulates frege systems, and that the constant-depth version of f-pc over finite field polynomially simulates constant-depth frege systems with modular counting. we also present a short constant-depth f-pc (in fact, f-ns) proof of the propositional pigeon-hole principle. finally, we introduce several extensions of our systems and pose numerous open questions.
how to whack moles. in the classical whack-a-mole game moles that pop up at certain locations must be whacked by means of a hammer before they go under ground again. the goal is to maximize the number of moles whacked. this problem can be formulated as an online optimization problem: requests (moles) appear over time at points in a metric space and must be served (whacked) by a server (hammer) before their deadlines (i.e., before they disappear). an online algorithm learns each request only at its release time and must base its decisions on incomplete information. we study the online whack-a-mole problem (wham) on the real line and on the uniform metric space. while on the line no deterministic algorithm can achieve a constant competitive ratio, we provide competitive algorithms for the uniform metric space. our online investigations are complemented by complexity results for the offline problem.
computability of the additive complexity of algebraic circuits with root extracting. we design an algorithm for computing the generalized (algebraic circuits with root extraction) {\em additive complexity} of any rational function. it is the first computability result of this sort on the additive complexity of algebraic circuits (cf.~\cite{sw80}).
authentication tests and the structure of bundles. suppose a principal in a cryptographic protocol creates and transmits a message containing a new value v, later receiving v back in a different cryptographic context. it can be concluded that some principal possessing the relevant key has received and transformed the message in which v was emitted. in some circumstances, this principal must be a regular participant of the protocol, not the penetrator. an inference of this kind is an authentication test. we introduce two main kinds of authentication test. an outgoing test is one in which the new value v is transmitted in encrypted form, and only a regular participant can extract it from that form. an incoming test is one in which v is received back in encrypted form, and only a regular participant can put it in that form. we combine these two tests with a supplementary idea, the unsolicited test, and a related method for checking that keys remain secret. together, these techniques determine what authentication properties are achieved by a wide range of cryptographic protocols. in this paper we introduce authentication tests and prove their soundness. we illustrate their power by giving new and straightforward proofs of security goals for several protocols. we also illustrate how to use the authentication tests as a heuristic for finding attacks against incorrect protocols. finally, we suggest a protocol design process. we express these ideas in the strand space formalism (thayer et al. j. comput. security 7 (1999) 191-230), which provides a convenient context to prove them correct.
on the algorithmic inversion of the discrete radon transform. the present paper deals with the computational complexity of the discrete inverse problem of reconstructing finite point sets and more general functionals with finite support that are accessible only through some of the values of their discrete radon transform. it turns out that this task behaves quite differently from its well-studied companion problem involving 1-dimensional x-rays. concentrating on the case of coordinate hyperplanes in rd and on functionals :zdd with d{{0,1,...,r},n0} for some arbitrary but fixed r, we show in particular that the problem can be solved in polynomial time if information is available for m such hyperplanes when md1 but is np-hard for m=d and d={0,1,...,r}. however, for d=n0, a case that is relevant in the context of contingency tables, the problem is still in p. similar results are given for the task of determining the uniqueness of a given solution and for a related counting problem.
a relation algebraic model of robust correctness. we propose a new and uniform abstract relational approach to demonic nondeterminism and robust correctness similar to hoare's chaos semantics. it is based on a specific set of relations on flat lattices. this set forms a complete lattice. furthermore, we deal with the refinement of programs. among other things, we show the correctness of the unfold/fold method for demonic nondeterminism and robust correctness as refinement relation and investigate relationships to dijkstra's wp-calculus and morgan's specification statement. &mdash;authors' abstract
chordless paths through three vertices. consider the following problem, which we call "chordless path through three vertices" or cp3v, for short: given a simple undirected graph g = (v, e), a positive integer k, and three distinct vertices s, t, and v ∈ v, is there a chordless path of length at most k from s via v to t in g? in a chordless path, no two vertices are connected by an edge that is not in the path. alternatively, one could say that the subgraph induced by the vertex set of the path in g is the path itself. the problem has arisen in the context of service deployment in communication networks. we resolve the parametric complexity of cp3v by proving it w[1]-complete with respect to its natural parameter k. our reduction extends to a number of related problems about chordless paths and cycles. in particular, deciding on the existence of a single directed chordless (s, t)-path in a digraph is also w[1]-complete with respect to the length of the path.
the parallel composition of uniform processes with data. a general basis for the definition of a finite but unbounded number of parallel processes is the equation s(n; dt)=p(0; get(0; dt)) &dgr; eq(n; 0). (p(n; get(n; dt)) //s(n&minus; 1; dt)). in this formula eq(n; 0) is an equality test, and get(n; dt) denotes the nth data element in table dt. we derive a linear process equation with the same behaviour as s(n; dt), and show that this equation is well-defined, provided one adopts the principle cl-rsp from bezem and groote proceedings of concur'94, springer, berlin, 1994, pp. 401-416). in order to demonstrate the strength of our result, we use it for the analysis of a standard example. we show that n + 1 concatenated buffers form a queue of capacity n + 1. copyright 2001 elsevier science b.v.
parameterised boolean equation systems. boolean equation system are a useful tool for verifying formulas from modal µ-calculus on transition systems (see [mader, lecture notes in computer science, vol. 1019, 1995, pp. 72-88] for an excellent treatment). we are interested in an extension of boolean equation systems with data. this allows to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. in previous works [groote and mateescu, lecture notes in computer science, vol. 1548, 1999, pp. 74-90; groote and willemse, sci. comput. program., 2005] it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised boolean equation system, or equation system for short. in this article we focus on techniques to solve such equation systems.we introduce a new equivalence between equation systems, because existing equivalences are not compositional. we present techniques similar to gauß elimination as outlined in [mader, lecture notes in computer science, vol. 1019, 1995, pp. 72-88] that allow to solve each equation system provided a single equation can be solved. we give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). finally, we provide several small but illustrative examples of verifications of modal µ-calculus formulas on concrete processes to show the use of the techniques.