32 Search Results for "Tiwari, Ashish"

Volume

LIPIcs, Volume 15

23rd International Conference on Rewriting Techniques and Applications (RTA'12)

RTA 2012, May 28 to June 2, 2012, Nagoya, Japan

Editors: Ashish Tiwari

Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2016.4
Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control (Invited Paper)

Authors: Junxing Yang, Radu Grosu, Scott A. Smolka, and Ashish Tiwari

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We present a new formulation of the V-formation problem for migrating birds in terms of model predictive control (MPC). In our approach, to drive a collection of birds towards a desired formation, an optimal velocity adjustment (acceleration) is performed at each time-step on each bird's current velocity using a model-based prediction window of $T$ time-steps. We present both centralized and distributed versions of this approach. The optimization criteria we consider are based on fitness metrics of candidate accelerations that birds in a V-formations are known to benefit from, including velocity matching, clear view, and upwash benefit. We validate our MPC-based approach by showing that for a significant majority of simulation runs, the flock succeeds in forming the desired formation. Our results help to better understand the emergent behavior of formation flight, and provide a control strategy for flocks of autonomous aerial vehicles.
Cite as

Junxing Yang, Radu Grosu, Scott A. Smolka, and Ashish Tiwari. Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 4:1-4:5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.CONCUR.2016.4,
  author =	{Yang, Junxing and Grosu, Radu and Smolka, Scott A. and Tiwari, Ashish},
  title =	{{Love Thy Neighbor: V-Formation as a Problem of Model Predictive Control}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{4:1--4:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.4},
  URN =		{urn:nbn:de:0030-drops-61896},
  doi =		{10.4230/LIPIcs.CONCUR.2016.4},
  annote =	{Keywords: bird flocking, v-formation, model predictive control, particle swarm optimization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.405
Two-Restricted One Context Unification is in Polynomial Time

Authors: Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
Cite as

Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-Restricted One Context Unification is in Polynomial Time. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 405-422, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gascon_et_al:LIPIcs.CSL.2015.405,
  author =	{Gasc\'{o}n, Adri\`{a} and Schmidt-Schau{\ss}, Manfred and Tiwari, Ashish},
  title =	{{Two-Restricted One Context Unification is in Polynomial Time}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{405--422},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.405},
  URN =		{urn:nbn:de:0030-drops-54289},
  doi =		{10.4230/LIPIcs.CSL.2015.405},
  annote =	{Keywords: context unification, first-order unification, deduction, type checking}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.RTA.2012
LIPIcs, Volume 15, RTA'12, Complete Volume

Authors: Ashish Tiwari

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
LIPIcs, Volume 15, RTA'12, Complete Volume
Cite as

Ashish Tiwari. LIPIcs, Volume 15, RTA'12, Complete Volume. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{tiwari:LIPIcs.RTA.2012,
  title =	{{LIPIcs, Volume 15, RTA'12, Complete Volume}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012},
  URN =		{urn:nbn:de:0030-drops-41090},
  doi =		{10.4230/LIPIcs.RTA.2012},
  annote =	{Keywords: Programming Techniques, Software Engineering, Programming Languages, Computation by Abstract Devices, Analysis of Algorithms and Problem Complexity Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Artificial Intelligence}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.RTA.2012.i
RTA 2012 Proceedings Frontmatter

Authors: Ashish Tiwari

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Frontmatter, Table of Contents, Conference Organization, External Reviewers, Author Index.
Cite as

Ashish Tiwari. RTA 2012 Proceedings Frontmatter. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. i-xiii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{tiwari:LIPIcs.RTA.2012.i,
  author =	{Tiwari, Ashish},
  title =	{{RTA 2012 Proceedings Frontmatter}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{i--xiii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.i},
  URN =		{urn:nbn:de:0030-drops-35033},
  doi =		{10.4230/LIPIcs.RTA.2012.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Conference Organization, External Reviewers, Author Index, RTA 2012, proceedings}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.RTA.2012.1
Computational Real Algebraic Geometry in Practice (Invited Talk)

Authors: Hirokazu Anai

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Real algebraic geometry deals with the solution set of (possibly quantified) systems of polynomial equations and/or inequalities over the real numbers, which arise frequently in science and engineering. Main concern in real algebraic geometry is to determine the properties of the solution sets such as non-emptiness, dimension and quantifier free description as a semi-algebraic set. Such tasks are carried out by symbolic and algebraic algorithms:cylindrical algebraic decomposition (CAD) or quantifier elimination (QE). Various algorithms and deep complexity results about CAD and QE have been studied during the last several decades. Moreover, practically efficient software systems of QE have been developed and also are applied to many nontrivial application problems. In this talk we explain several algorithms of CAD and QE together with their engineering applications.
Cite as

Hirokazu Anai. Computational Real Algebraic Geometry in Practice (Invited Talk). In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, p. 1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{anai:LIPIcs.RTA.2012.1,
  author =	{Anai, Hirokazu},
  title =	{{Computational Real Algebraic Geometry in Practice}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{1--1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.1},
  URN =		{urn:nbn:de:0030-drops-34784},
  doi =		{10.4230/LIPIcs.RTA.2012.1},
  annote =	{Keywords: real algebraic geometry, quantifier elimination, cylindrical algebraic decomposition, symbolic optimization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.RTA.2012.2
Rho-Calculi for Computation and Logic (Invited Talk)

Authors: Claude Kirchner

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
The rho-calculi provide enlightening concepts for both computing and reasoning as well as their combination. They consist in the generalization of lambda-calculus to structures like terms, propositions or graphs and we will show how their interrelations with deduction provide powerful frameworks for the next generation of proof assistants.
Cite as

Claude Kirchner. Rho-Calculi for Computation and Logic (Invited Talk). In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 2-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kirchner:LIPIcs.RTA.2012.2,
  author =	{Kirchner, Claude},
  title =	{{Rho-Calculi for Computation and Logic}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{2--4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.2},
  URN =		{urn:nbn:de:0030-drops-34796},
  doi =		{10.4230/LIPIcs.RTA.2012.2},
  annote =	{Keywords: rewriting calculus, rho-calculus, deduction modulo}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.RTA.2012.5
Dictionary-Based Tree Compression (Invited Talk)

Authors: Sebastian Maneth

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Trees are a ubiquitous data structure in computer science. LISP, for instance, was designed to manipulate nested lists, that is, ordered unranked trees. Already at that time, DAGs were used to detect common subexpression, a process known as "hash consing." In a DAG every distinct subtree is represented only once (but can be referenced many times) and hence it constitutes a dictionary-based compression method for ordered trees. In our compression scenario we distinguish two kinds of ordered trees: binary and unranked. The latter appear naturally as representation of XML document structures. We survey these dictionary-based compression methods for ordered trees: (1) DAGs, (2) hybrid DAGs, (3) straight-line context-free tree grammars ("SLT grammars"). We compare the minimal DAG of an unranked tree with the minimal DAG of its binary tree encoding. The latter is obtained by identifying first children of the unranked tree with left children of the binary tree, and next-siblings with the right children. For XML document trees, unranked DAGs are usually smaller than encoded binary DAGs. We show that this holds for arbitrary unranked trees, on average. We also present the "hybrid DAG"; its size lower-bounds those of the binary and unranked DAGs. Finding a smallest SLT grammar for a given tree is NP-complete. We discuss two linear-time approximation algorithms: BPLEX and TreeRePair. For typical XML document trees, TreeRePair produces SLT grammars that are only one fourth of the size of the minimal DAG, and which contain approximately 3$% of the edges of the original tree. As far as we know, this gives rise to the smallest existing pointer-based tree representation. We show that some basic algorithms can be computed directly on the compressed trees, without prior decompression. Examples include the execution of different kinds of tree automata, and the real-time traversal of the original tree. It is even possible to evaluate simple XPath queries directly on the SLT grammars, using deterministic node-selecting tree automata. In this way, impressive speed-ups are achieved over existing XPath evaluators, while at the same time the memory requirement is slashed to only a few percent. For more complex XPath queries that require nondeterministic node-selecting tree automata, efficient evaluation over SLT grammars remains a difficult challenge.
Cite as

Sebastian Maneth. Dictionary-Based Tree Compression (Invited Talk). In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, p. 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{maneth:LIPIcs.RTA.2012.5,
  author =	{Maneth, Sebastian},
  title =	{{Dictionary-Based Tree Compression}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{5--5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.5},
  URN =		{urn:nbn:de:0030-drops-34802},
  doi =		{10.4230/LIPIcs.RTA.2012.5},
  annote =	{Keywords: Tree grammars, tree automata, straight-line programs}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.6
An Abstract Factorization Theorem for Explicit Substitutions

Authors: Beniamino Accattoli

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We study a simple form of standardization, here called factorization, for explicit substitutions calculi, i.e. lambda-calculi where beta-reduction is decomposed in various rules. These calculi, despite being non-terminating and non-orthogonal, have a key feature: each rule terminates when considered separately. It is well-known that the study of rewriting properties simplifies in presence of termination (e.g. confluence reduces to local confluence). This remark is exploited to develop an abstract theorem deducing factorization from some axioms on local diagrams. The axioms are simple and easy to check, in particular they do not mention residuals. The abstract theorem is then applied to some explicit substitution calculi related to Proof-Nets. We show how to recover standardization by levels, we model both call-by-name and call-by-value calculi and we characterize linear head reduction via a factorization theorem for a linear calculus of substitutions.
Cite as

Beniamino Accattoli. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 6-21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{accattoli:LIPIcs.RTA.2012.6,
  author =	{Accattoli, Beniamino},
  title =	{{An Abstract Factorization Theorem for Explicit Substitutions}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{6--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.6},
  URN =		{urn:nbn:de:0030-drops-34813},
  doi =		{10.4230/LIPIcs.RTA.2012.6},
  annote =	{Keywords: lambda-calculus, Standardization, Explicit Substitutions, Abstract rewriting, Diagrammatic reasoning}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.22
On the Invariance of the Unitary Cost Model for Head Reduction

Authors: Beniamino Accattoli and Ugo Dal Lago

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
The lambda-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. In this paper, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the lambda-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies the unitary cost model is invariant, if any.
Cite as

Beniamino Accattoli and Ugo Dal Lago. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 22-37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.RTA.2012.22,
  author =	{Accattoli, Beniamino and Dal Lago, Ugo},
  title =	{{On the Invariance of the Unitary Cost Model for Head Reduction}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{22--37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.22},
  URN =		{urn:nbn:de:0030-drops-34820},
  doi =		{10.4230/LIPIcs.RTA.2012.22},
  annote =	{Keywords: lambda calculus, cost models, explicit substitutions, implicit computational complexity}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.38
A Term Rewriting System for Kuratowski's Closure-Complement Problem

Authors: Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, and Volker Sorge

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We present a term rewriting system to solve a class of open problems that are generalisations of Kuratowski's closure-complement theorem. The problems are concerned with finding the number of distinct sets that can be obtained by applying combinations of axiomatically defined set operators. While the original problem considers only closure and complement of a topological space as operators, it can be generalised by adding operators and varying axiomatisation. We model these axioms as rewrite rules and construct a rewriting system that allows us to close some so far open variants of Kuratowski's problem by analysing several million inference steps on a typical personal computer.
Cite as

Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, and Volker Sorge. A Term Rewriting System for Kuratowski's Closure-Complement Problem. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 38-52, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{alhassani_et_al:LIPIcs.RTA.2012.38,
  author =	{Al-Hassani, Osama and Mahesar, Quratul-ain and Sacerdoti Coen, Claudio and Sorge, Volker},
  title =	{{A Term Rewriting System for Kuratowski's Closure-Complement Problem}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{38--52},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.38},
  URN =		{urn:nbn:de:0030-drops-34838},
  doi =		{10.4230/LIPIcs.RTA.2012.38},
  annote =	{Keywords: Kuratowski's closure-complement problem, Rewriting system}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.53
Term Rewriting Systems as Topological Dynamical Systems

Authors: Soren Bjerg Andersen and Jakob Grue Simonsen

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Topological dynamics is, roughly, the study of phenomena related to iterations of continuous maps from a metric space to itself. We show how the rewrite relation in term rewriting gives rise to dynamical systems in two distinct, natural ways: (A) One in which any deterministic rewriting strategy induces a dynamical system on the set of finite and infinite terms endowed with the usual metric, and (B) one in which the unconstrained rewriting relation induces a dynamical system on sets of sets of terms, specifically the set of compact subsets of the set of finite and infinite terms endowed with the Hausdorff metric. For both approaches, we give sufficient criteria for the induced systems to be well-defined dynamical systems and for (A) we demonstrate how the classic topological invariant called topological entropy turns out to be much less useful in the setting of term rewriting systems than in symbolic dynamics.
Cite as

Soren Bjerg Andersen and Jakob Grue Simonsen. Term Rewriting Systems as Topological Dynamical Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 53-68, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{andersen_et_al:LIPIcs.RTA.2012.53,
  author =	{Andersen, Soren Bjerg and Simonsen, Jakob Grue},
  title =	{{Term Rewriting Systems as Topological Dynamical Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{53--68},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.53},
  URN =		{urn:nbn:de:0030-drops-34841},
  doi =		{10.4230/LIPIcs.RTA.2012.53},
  annote =	{Keywords: Term rewriting, dynamical systems, topology, symbolic dynamics}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.69
Infinitary Term Graph Rewriting is Simple, Sound and Complete

Authors: Patrick Bahr

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.
Cite as

Patrick Bahr. Infinitary Term Graph Rewriting is Simple, Sound and Complete. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 69-84, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2012.69,
  author =	{Bahr, Patrick},
  title =	{{Infinitary Term Graph Rewriting is Simple, Sound and Complete}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{69--84},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.69},
  URN =		{urn:nbn:de:0030-drops-34857},
  doi =		{10.4230/LIPIcs.RTA.2012.69},
  annote =	{Keywords: term graphs, infinitary rewriting}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.85
Axiomatic Sharing-via-Labelling

Authors: Thibaut Balabonski

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
A judicious use of labelled terms makes it possible to bring together the simplicity of term rewriting and the sharing power of graph rewriting: this has been known for twenty years in the particular case of orthogonal first-order systems. The present paper introduces a concise and easily usable axiomatic presentation of sharing-via-labelling techniques that applies to higher-order term rewriting as well as to non-orthogonal term rewriting. This provides a general framework for the sharing of subterms and keeps the formalism as simple as term rewriting.
Cite as

Thibaut Balabonski. Axiomatic Sharing-via-Labelling. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 85-100, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{balabonski:LIPIcs.RTA.2012.85,
  author =	{Balabonski, Thibaut},
  title =	{{Axiomatic Sharing-via-Labelling}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{85--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.85},
  URN =		{urn:nbn:de:0030-drops-34868},
  doi =		{10.4230/LIPIcs.RTA.2012.85},
  annote =	{Keywords: Sharing, Abstract term rewriting, Graphs, Higher order, Non-orthogonality}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.101
On the Decidability Status of Reachability and Coverability in Graph Transformation Systems

Authors: Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier, and Jan Stückrath

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
We study decidability issues for reachability problems in graph transformation systems, a powerful infinite-state model. For a fixed initial configuration, we consider reachability of an entirely specified configuration and of a configuration that satisfies a given pattern (coverability). The former is a fundamental problem for any computational model, the latter is strictly related to verification of safety properties in which the pattern specifies an infinite set of bad configurations. In this paper we reformulate results obtained, e.g., for context-free graph grammars and concurrency models, such as Petri nets, in the more general setting of graph transformation systems and study new results for classes of models obtained by adding constraints on the form of reduction rules.
Cite as

Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier, and Jan Stückrath. On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 101-116, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.RTA.2012.101,
  author =	{Bertrand, Nathalie and Delzanno, Giorgio and K\"{o}nig, Barbara and Sangnier, Arnaud and St\"{u}ckrath, Jan},
  title =	{{On the Decidability Status of Reachability and Coverability in  Graph Transformation Systems}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{101--116},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.101},
  URN =		{urn:nbn:de:0030-drops-34871},
  doi =		{10.4230/LIPIcs.RTA.2012.101},
  annote =	{Keywords: decidability, reachability, graph transformation, coverability}
}
  • Refine by Author
  • 6 Tiwari, Ashish
  • 2 Accattoli, Beniamino
  • 2 Schmidt-Schauß, Manfred
  • 1 Al-Hassani, Osama
  • 1 Allais, Guillaume
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 decidability
  • 2 infinitary rewriting
  • 2 term rewriting
  • 2 termination
  • 1 (pre-)Heyting algebras
  • Show More...

  • Refine by Type
  • 31 document
  • 1 volume

  • Refine by Publication Year
  • 27 2012
  • 1 2009
  • 1 2011
  • 1 2013
  • 1 2015
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact