waashk/dblp huggingface dataset:
equational theories of tropical semirings. this paper studies the equational theories of various exotic semirings presented in the literature. exotic semirings are semirings whose underlying carrier set is some subset of the set of real numbers equipped with binary operations of minimum or maximum as sum, and addition as product. two prime examples of such structures are the (max,+) semiring and the tropical semiring. it is shown that none of the exotic semirings commonly considered in the literature has a finite basis for its equations, and that similar results hold for the commutative idempotent weak semirings that underlie them. for each of these commutative idempotent weak semirings, the paper offers characterizations of the equations that hold in them, decidability results for their equational theories, explicit descriptions of the free algebras in the varieties they generate, and relative axiomatization results.
regular closed sets of permutations. machines whose main purpose is to permute and sort data are studied. the sets of permtutations that can arise are analysed by means of finite automata and avoided pattern techniques. conditions are given for these sets to be enumerated by rational generating functions. as a consequence we give the first non-trivial examples of pattern closed sets of permutations all of whose closed subclasses have rational generating functions.
longest increasing subsequences in sliding windows. we consider the problem of finding the longest increasing subsequence in a sliding window over a given sequence (lisw). we propose an output-sensitive data structure that solves this problem in time o(n log log n+output) for a sequence of n elements. this data structure substantially improves over the naïve generalization of the longest increasing subsequence algorithm and in fact produces an output-sensitive optimal solution.
ccs with hennessy's merge has no finite-equational axiomatization. this paper confirms a conjecture of bergstra and klop's from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by hennessy in 1981 to the recursion free fragment of milner's calculus of communicating systems is not finitely based modulo bisimulation equivalence. thus, hennessy's merge cannot replace the left merge and communication merge operators proposed by bergstra and klop, at least if a finite axiomatization of parallel composition modulo bisimulation equivalence is desired.
normal form algorithms for extended context-free grammars. we investigate the complexity of a variety of normal-form transformations for extended context-free grammars, where by extended we mean that the set of right-hand sides for each nonterminal in such a grammar is a regular set. the study is motivated by the implementation project grama which will provide a c++ toolkit for the symbolic manipulation of context-free objects just as grail does for regular objects. our results generalize known complexity bounds for context-free grammars but do so in nontrivial ways. specifically, we introduce a new representation scheme for extended context-free grammars (the symbol-threaded expression forest), a new normal form for these grammars (dot normal form) and new regular expression algorithms. copyright 2001 elsevier science b.v.
bisimilarity is not finitely based over bpa with interrupt. this paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching bergstra and klop's basic process algebra (bpa) with the interrupt operator. moreover, it is shown that the collection of closed equations over this language is also not finitely based. in sharp contrast to these results, the collection of closed equations over the language bpa enriched with the disrupt operator is proven to be finitely based.
a complete equational axiomatization for mpa with string iteration. we study equational axiomatizations of bisimulation equivalence for the language obtained by extending milner''s basic ccs with string iteration. string iteration is a variation on the original binary version of the kleene star operation $p^* q$ obtained by restricting the first argument to be a non-empty sequence of atomic actions. we show that, for every positive integer $k$, bisimulation equivalence over the set of processes in this language with loops of length at most $k$ is finitely axiomatizable, provided that the set of actions is finite. we also offer an infinite equational theory that completely axiomatizes bisimulation equivalence over the whole language. we prove that this result cannot be improved upon by showing that no finite equational axiomatization of bisimulation equivalence over basic ccs with string iteration can exist, unless the set of actions is empty.
a calculus for reasoning about software composition. although the term software component has become commonplace, there is no universally accepted definition of the term, nor does there exist a common foundation for specifying various kinds of components and their compositions. we propose such a foundation. the piccola calculus is a process calculus, based on the asynchronous π-calculus, extended with explicit namespaces. the calculus is high level, rather than minimal, and is consequently convenient for expressing and reasoning about software components, and different styles of composition. we motivate and present the calculus, and outline how it is used to specify the semantics of piccola, a small composition language. we demonstrate how the calculus can be used to simplify compositions by partial evaluation, and we briefly outline some other applications of the calculus to reasoning about compositional styles.
lower bounds for random 3-sat via differential equations. it is widely believed that the probability of satisfiability for random k-sat formulae exhibits a sharp threshold as a function of their clauses-to-variables ratio. for the most studied case, k= 3, there have been a number of results during the last decade providing upper and lower bounds for the threshold's potential location. all lower bounds in this vein have been algorithmic, i.e., in each case a particular algorithm was shown to satisfy random instances of 3-sat with probability 1- o(1) if the clauses-to-variables ratio is below a certain value. we show how differential equations can serve as a generic tool for analyzing such algorithms by rederiving most of the known lower bounds for random 3-sat in a simple, uniform manner.
on coalgebra based on classes. the category class of classes and functions is proved to have a number of properties suitable for algebra and coalgebra: every endofunctor is set-based, it has an initial algebra and a terminal coalgebra, the categories of algebras and coalgebras are complete and cocomplete, and every endofunctor generates a free completely iterative monad. a description of a terminal coalgebra for the power-set functor is provided.
on tree coalgebras and coalgebra presentations. for deterministic systems, expressed as coalgebras over polynomial functors, every tree t (an element of the final coalgebra) turns out to represent a new coalgebra at. the universal property of this family of coalgebras, resembling freeness, is that for every state s of every system s there exists a unique coalgebra homomorphism from a unique at which takes the root of t to s. consequently, the tree coalgebras are finitely presentable and form a strong generator. thus, these categories of coalgebras are locally finitely presentable; in particular every system is a filtered colimit of finitely presentable systems.in contrast, for transition systems expressed as coalgebras over the finite-power-set functor we show that there are systems which fail to be filtered colimits of finitely presentable (=finite) ones.surprisingly, if λ is an uncountable cardinal, then λ-presentation is always well-behaved: whenever an endofunctor f preserves λ-filtered colimits (i.e., is λ-accessible), then λ-presentable coalgebras are precisely those whose underlying objects are λ-presentable. consequently, every f coalgebra is a λ-filtered colimit of λ-presentable coalgebras; thus coalg f is a locally λ-presentable category. (this holds for all endofunctors of λ-accessible categories with colimits of ω-chains.) corollary: a set functor is bounded at λ in: the sense of kawahara and mori iff it is λ+-accessible.
on the usability of process algebra: an architectural view. despite its strengths like compositionality and equivalence checking, process algebra is rarely adopted outside the academia. in this paper we address the usability issue for process algebra along two different directions. on the modeling side, we provide a set of guidelines inspired by the software architecture field, which should enforce a clear component-oriented approach to the process algebraic design of system families. on the verification side, we propose a component-oriented technique based on equivalence checking for the detection of architecture-level mismatches and the provision of related diagnostic information. such a technique extends previous results in terms of generality of the considered mismatches, generality of the considered system topologies, and scalability to system families.
permuting machines and priority queues. machines whose sole function is to re-order their input data are considered. every such machine defines a set of allowable input-output pairs of permutations. these sets are studied in terms of the minimal disallowed pairs (the basis). some allowable sets with small bases are considered including the one defined by a priority queue machine. for more complex machines defined by two or more priority queues in series or parallel, the basis is proved to be infinite.
mutilated chessboard problem is exponentially hard for resolution. mutilated chessboard principle cbn says that it is impossible to cover by domino tiles the chessboard 2n × 2n with two diagonally opposite corners removed. we prove 2ω(√n) lower bound on the size of minimal resolution refutation of cbn.
coloring octrees. an octree is a recursive partition of the unit cube, such that in each step a cube is subdivided into eight smaller cubes. those cubes that are not further subdivided are the leaves of the octree. we consider the problem of coloring the leaves of an octree using as few colors as possible such that no two of them get the same color if they share a facet. it turns out that the number of colors needed depends on a parameter that we call unbalancedness. roughly speaking, this parameter measures how much adjacent cubes differ in size. for most values of this parameter we give tight bounds on the minimum number of colors, and extend the results to higher dimensions.
a new logic for electronic commerce protocols. the primary objective of this paper is to present the definition of a new dynamic, linear and modal logic for security protocols. the logic is compact, expressive and formal. it allows the specification of classical security properties (authentication, secrecy and integrity) and also electronic commerce properties (non-repudiation, anonymity, good atomicity, money atomicity, certified delivery, etc.). the logic constructs are interpreted over a trace-based model. traces reflect valid protocol executions in the presence of a malicious smart intruder. the logic is endowed with a tableau-based proof system that leads to a modular denotational semantics and local model checking.
divisibility problem for one relator monoids. we describe an algorithm which partially solves the divisibility problem for monoids with one defining relation of a special form. it can be shown that the word problem for one-relator monoids can be reduced to the problem studied here. it is conjectured that the presented algorithm can be completed to an algorithm which gives full solution of the problem. the validity of the conjecture would imply the decidability of the word problem for one-relator monoids.
intersection types and lambda models. invariance of interpretation by β-conversion is one of the minimal requirements for any standard model for the λ-calculus. with the intersection-type systems being a general framework for the study of semantic domains for the λ-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results ibr intersection-type assignment systems.instead of considering conversion as a whole, reduction and expansion will be considered separately. not only for usual computational rules like β η, but also for a number of relevant restrictions of those. characterisations will be also provided for (intersection) filter structures that are indeed λ-models.
a category of compositional domain-models for separable stone spaces. in this paper we introduce sfpm, a category of sfp domains which provides very satisfactory domain-models, i.e. "partializations", of separable stone spaces (2-stone spaces). more specifically, sfpm is a subcategory of sfpep, closed under direct limits as well as many constructors, such as lifting, sum, product and plotkin powerdomain (with the notable exception of the function space constructor). sfpm is "structurally well behaved", in the sense that the functor max, which associates to each object of sfpm the stone space of its maximal elements, is compositional with respect to the constructors above, and ω-continuous. a correspondence can be established between these constructors over sfpm and appropriate constructors on stone spaces, whereby sfpm domain-models of stone spaces defined as solutions of a vast class of recursive equations in sfpm, can be obtained simply by solving the corresponding equations in sfpm. moreover any continuous function between two 2-stone spaces can be extended to a continuous function between any two sfpm domain-models of the original spaces. the category sfpm does not include all the sfp's with a 2-stone space of maximal elements (csfp's). we show that the csfp's can be characterized precisely as suitable retracts of sfpm objects. then the results proved for sfpm easily extends to the wider category having csfp's as objects.using sfpm we can provide a plethora of "partializations" of the space of finitary hypersets (the hyperuniverse nω (ann. new york acad. sci. 806 (1996) 140). these includes the classical ones proposed in abramsky (a cook's tour of the finitary non-well-founded sets unpublished manuscript, 1988; inform. comput. 92(2) (1991) 161) and mislove et al. (inform. comput. 93(1) (1991) 16), which are also shown to be non-isomorphic, thus providing a negative answer to a problem raised in mislove et al.
an arithmetic for non-size-increasing polynomial-time computation. an arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of gödel's t and therefore defines a non-size-increasing polynomial time computable function.
intersection types and domain operators. we use intersection types as a tool for obtaining λ-models. relying on the notion of easy intersection type theory, we successfully build a λ-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. this allows us to prove two results. the first gives a proof of consistency of the λ-theory where the λ-term (λx.xx)(λx.xx) is forced to behave as the join operator. this result has interesting consequences on the algebraic structure of the lattice of λ-theories. the second result is that for any simple easy term, there is a λ-model, where the interpretation of the term is the minimal fixed point operator.
model checking discounted temporal properties. temporal logic is two-valued: formulas are interpreted as either true or false. when applied to the analysis of stochastic systems, or systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for a specification. we present a generalization of the branching-time logic ctl which achieves robustness with respect to model perturbations by giving a quantitative interpretation to predicates and logical operators, and by discounting the importance of events according to how late they occur. in every state, the value of a formula is a real number in the interval [0,1], where 1 corresponds to truth and 0 to falsehood. the boolean operators and and or are replaced by min and max, the path quantifiers ∃ and ¬ determine sup and inf over all paths from a given state, and the temporal operators ♦ and □ specify sup and inf over a given path; a new operator averages all values along a path. furthermore, all path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path.we interpret the resulting logic dctl over transition systems, markov chains, and markov decision processes. we present two semantics for dctl: a path semantics, inspired by the standard interpretation of state and path formulas in ctl, and a fixpoint semantics, inspired by the µ-calculus evaluation of ctl formulas. we show that, while these semantics coincide for ctl, they differ for dctl, and we provide model-checking algorithms for both semantics.
hybrid diagrams. hybrid systems provide a formal model for physical systems controlled by discrete-state controllers. to help with the design of correct controllers, we present a methodology that enables the verification of linear-time temporal logic properties of general, non-linear hybrid systems. the methodology is based on the deductive transformation and algorithmic checking of hybrid diagrams.hybrid diagrams are graphs whose vertices and edges are labeled with first-order assertions; they represent system abstractions, together with the progress properties that have been proved about them. the verification process begins with the automatic construction of an initial diagram, whose behavior coincides with that of the hybrid system. the proof of a specification is constructed by applying a series of diagram transformations to this initial diagram. the transformations preserve behavior containment, and the aim of the transformations is to obtain a diagram that can be algorithmically shown to satisfy the specification. whenever the algorithmic check of a diagram fails, the check returns guidance for the further transformation of the diagram, or indications about possible counterexamples to the specification.we present four rules for transforming diagrams: each rule enables the study of a certain class of temporal logic properties. while some rules can be applied unconditionally, others require the proof of first-order verification conditions. we prove that the rules lead to the first verification methodology for general hybrid systems that is complete (relative to first-order reasoning) for proving specifications expressed in first-order linear-time temporal logic, provided no temporal operator appears in the scope of a quantifier.
an optimal pre-determinization algorithm for weighted transducers. we present a general algorithm, pre-determinization, that makes an arbitrary weighted transducer over the tropical semiring or an arbitrary unambiguous weighted transducer over a cancellative commutative semiring determinizable by inserting in it transitions labeled with special symbols. after determinization, the special symbols can be removed or replaced with ε-transitions. the resulting transducer can be significantly more efficient to use. we report empirical results showing that our algorithm leads to a substantial speed-up in large-vocabulary speech recognition. our pre-determinization algorithm makes use of an efficient algorithm for testing a general twins property, a sufficient condition for the determinizability of all weighted transducers over the tropical semiring and unambiguous weighted transducers over cancellative commutative semirings. based on the transitions marked by this test of the twins property, our pre-determinization algorithm inserts new transitions just when needed to guarantee that the resulting transducer has the twins property and thus is determinizable. it also uses a single-source shortest-paths algorithm over the min-max semiring for carefully selecting the positions for insertion of new transitions to benefit from the subsequent application of determinization. these positions are proved to be optimal in a sense that we describe.
nl-printable sets and nondeterministic kolmogorov complexity. p-printable sets were defined by hartmanis and yesha and have been investigated by several researchers. the analogous notion of l-printable sets was defined by fortnow et al.; both p-printability and l-printability were shown to be related to notions of resource-bounded kolmogorov complexity. nondeterministic logspace (nl)-printability was defined by jenner and kirsig, but some basic questions regarding this notion were left open. in this paper we answer a question of jenner and kirsig by providing a machine-based characterization of the nl-printable sets.in order to relate nl-printability to resource-bounded kolmogorov complexity, the paper introduces nondeterministic space-bounded kolmogorov complexity. we present some of the basic properties of this notion of kolmogorov complexity.using similar techniques, we investigate relationships among classes between nl and ul.
palindrome complexity. we study the palindrome complexity of infinite sequences on finite alphabets, i.e., the number of palindromic factors (blocks) of given length occurring in a given sequence. we survey the known results and obtain new results for some sequences, in particular for rote sequences and for fixed points of primitive morphisms of constant length belonging to "class p" of hof-knill-simon. we also give an upper bound for the palindrome complexity of a sequence in terms of its (block-)complexity.
branching bisimulation for probabilistic systems: characteristics and decidability. we address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of hansson. in particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. we show that both alternatives coincide with branching bisimilarity. the alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. coloured trace equivalence can be understood without knowledge of probability theory and is independent of the notion of a scheduler. branching bisimilarity, rephrased in terms of maximal probabilities gives rise to an algorithm of polynomial complexity for deciding the equivalence. together they give a better understanding of branching bisimilarity. furthermore, we show that the notions of branching bisimilarity in the alternating model of hansson and in the nonalternating model of segala differ: branching bisimilarity in the latter setting turns out to discriminate between systems that are intuitively branching bisimilar.
the ring of k-regular sequences, ii. in this paper, we continue our study of k-regular sequences begun in 1992. we prove some new results, give many new examples from the literature, and state some open problems.