9 Search Results for "Praveen, M."


Document
Constraint LTL with Remote Access

Authors: Ashwin Bhaskar and M. Praveen

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)


Abstract
Constraint Linear Temporal Logic (CLTL) is an extension of LTL that is interpreted on sequences of valuations of variables over an infinite domain. The atomic formulas are interpreted as constraints on the valuations. The atomic formulas can constrain valuations at the current position and positions that are a fixed distance apart (e.g., the previous position or the second previous position and so on). The satisfiability problem for CLTL is known to be Pspace-complete. We generalize CLTL to let atomic formulas access positions that are unboundedly far away in the past. We annotate the sequence of valuations with letters from a finite alphabet and use regular expressions on the finite alphabet to control how atomic formulas access past positions. We prove that the satisfiability problem for this extension of the logic is decidable in cases where the domain is dense and open with respect to a linear order (e.g., rational numbers with the usual linear order). We prove that it is also decidable over integers with linear order and equality.

Cite as

Ashwin Bhaskar and M. Praveen. Constraint LTL with Remote Access. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 41:1-41:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2023.41,
  author =	{Bhaskar, Ashwin and Praveen, M.},
  title =	{{Constraint LTL with Remote Access}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{41:1--41:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.41},
  URN =		{urn:nbn:de:0030-drops-194142},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.41},
  annote =	{Keywords: Constraint LTL, Regular Expressions, MSO formulas, Satisfiability, B\"{u}chi automata}
}
Document
Realizability Problem for Constraint LTL

Authors: Ashwin Bhaskar and M. Praveen

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


Abstract
Constraint linear-time temporal logic (CLTL) is an extension of LTL that is interpreted on sequences of valuations of variables over an infinite domain. The atomic formulas are interpreted as constraints on the valuations. The atomic formulas can constrain valuations over a range of positions along a sequence, with the range being bounded by a parameter depending on the formula. The satisfiability and model checking problems for CLTL have been studied by Demri and D’Souza. We consider the realizability problem for CLTL. The set of variables is partitioned into two parts, with each part controlled by a player. Players take turns to choose valuations for their variables, generating a sequence of valuations. The winning condition is specified by a CLTL formula - the first player wins if the sequence of valuations satisfies the specified formula. We study the decidability of checking whether the first player has a winning strategy in the realizability game for a given CLTL formula. We prove that it is decidable in the case where the domain satisfies the completion property, a property introduced by Balbiani and Condotta in the context of satisfiability. We prove that it is undecidable over (ℤ, < , =), the domain of integers with order and equality. We prove that over (ℤ, < , =), it is decidable if the atomic constraints in the formula can only constrain the current valuations of variables belonging to the second player, but there are no such restrictions for the variables belonging to the first player. We call this single-sided games.

Cite as

Ashwin Bhaskar and M. Praveen. Realizability Problem for Constraint LTL. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:LIPIcs.TIME.2022.8,
  author =	{Bhaskar, Ashwin and Praveen, M.},
  title =	{{Realizability Problem for Constraint LTL}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.8},
  URN =		{urn:nbn:de:0030-drops-172556},
  doi =		{10.4230/LIPIcs.TIME.2022.8},
  annote =	{Keywords: Realizability, constraint LTL, Strategy trees, Tree automata}
}
Document
Physical Modeling of Process Forces in Grinding

Authors: Praveen Sridhar, Daniel Mannherz, Raphael Bilz, Kristin M. de Payrebrune, Mahesh R.G. Prasad, and Juan Manuel Rodríguez Prieto

Published in: OASIcs, Volume 89, 2nd International Conference of the DFG International Research Training Group 2057 – Physical Modeling for Virtual Manufacturing (iPMVM 2020)


Abstract
This paper deals with material removal mechanisms in grinding by considering single grit-workpiece interactions. Individual investigations were performed both experimentally and using finite element simulations. Firstly, a comparison between the Johnson-Cooke material model and a Crystal Plasticity finite element method was performed with the help of micro-indentation experiments. Here the research question was answered if an anisotropic material model better describe the grinding process and process forces compared to an isotropic material model. Secondly, four discretization approaches were employed: pure Lagrangian (LAG), Arbitrary Lagrange Eulerian (ALE), Particle Finite Element Method (PFEM), and Smooth Particle Hydrodynamics (SPH), to simulate a micro-cutting operation of A2024 T351 aluminium. This study aims to compare the conventional approaches (LAG and ALE) to newer approaches (PFEM and SPH). The orthogonal cutting models were benchmarked against a micro-cutting experiment presented in literature, by comparing the obtained cutting and passive forces. The study was then extended to negative rake angles to study the effect on the discretization approaches for grinding. Thirdly, scratch experiments were investigated for a brittle material sodalime glass and A2024 T351 aluminium. Effects of the linear speed of the device, depth of cut, and conical tool angle were analyzed and tendencies are built. Finally, a realistic simulation of the manufacturing process of a grinding wheel was developed, starting with the raw material, compression, sintering, and dressing until the final grinding surface. As a result of the simulations, virtual grinding wheel topographies can be visualized and analyzed with regard to the output variables from grinding wheels such as bonding strength and static grain count. The individual research studies help in understanding the material removal mechanisms in a single grit scratch process as well as in the understanding of the overall grinding wheel topography. This in turn helps in the developing an overall physical force model for scratching/grinding to predict mechanical output parameters and hence reduce the need for experimentation.

Cite as

Praveen Sridhar, Daniel Mannherz, Raphael Bilz, Kristin M. de Payrebrune, Mahesh R.G. Prasad, and Juan Manuel Rodríguez Prieto. Physical Modeling of Process Forces in Grinding. In 2nd International Conference of the DFG International Research Training Group 2057 – Physical Modeling for Virtual Manufacturing (iPMVM 2020). Open Access Series in Informatics (OASIcs), Volume 89, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{sridhar_et_al:OASIcs.iPMVM.2020.16,
  author =	{Sridhar, Praveen and Mannherz, Daniel and Bilz, Raphael and de Payrebrune, Kristin M. and Prasad, Mahesh R.G. and Prieto, Juan Manuel Rodr{\'\i}guez},
  title =	{{Physical Modeling of Process Forces in Grinding}},
  booktitle =	{2nd International Conference of the DFG International Research Training Group 2057 – Physical Modeling for Virtual Manufacturing (iPMVM 2020)},
  pages =	{16:1--16:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-183-2},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{89},
  editor =	{Garth, Christoph and Aurich, Jan C. and Linke, Barbara and M\"{u}ller, Ralf and Ravani, Bahram and Weber, Gunther H. and Kirsch, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.iPMVM.2020.16},
  URN =		{urn:nbn:de:0030-drops-137651},
  doi =		{10.4230/OASIcs.iPMVM.2020.16},
  annote =	{Keywords: grinding, single grit approach, finite element method, smooth particle hydrodynamics, particle finite element method, scratch experiments, virtual grinding wheel model}
}
Document
What You Must Remember When Transforming Datawords

Authors: M. Praveen

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)


Abstract
Streaming Data String Transducers (SDSTs) were introduced to model a class of imperative and a class of functional programs, manipulating lists of data items. These can be used to write commonly used routines such as insert, delete and reverse. SDSTs can handle data values from a potentially infinite data domain. The model of Streaming String Transducers (SSTs) is the fragment of SDSTs where the infinite data domain is dropped and only finite alphabets are considered. SSTs have been much studied from a language theoretical point of view. We introduce data back into SSTs, just like data was introduced to finite state automata to get register automata. The result is Streaming String Register Transducers (SSRTs), which is a subclass of SDSTs. We use origin semantics for SSRTs and give a machine independent characterization, along the lines of Myhill-Nerode theorem. Machine independent characterizations for similar models are the basis of learning algorithms and enable us to understand fragments of the models. Origin semantics of transducers track which positions of the output originate from which positions of the input. Although a restriction, using origin semantics is well justified and is known to simplify many problems related to transducers. We use origin semantics as a technical building block, in addition to characterizations of deterministic register automata. However, we need to build more on top of these to overcome some challenges unique to SSRTs.

Cite as

M. Praveen. What You Must Remember When Transforming Datawords. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 55:1-55:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{praveen:LIPIcs.FSTTCS.2020.55,
  author =	{Praveen, M.},
  title =	{{What You Must Remember When Transforming Datawords}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{55:1--55:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.55},
  URN =		{urn:nbn:de:0030-drops-132967},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.55},
  annote =	{Keywords: Streaming String Transducers, Data words, Machine independent characterization}
}
Document
Query Preserving Watermarking Schemes for Locally Treelike Databases

Authors: Agnishom Chattopadhyay and M. Praveen

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)


Abstract
Watermarking is a way of embedding information in digital documents. Much research has been done on techniques for watermarking relational databases and XML documents, where the process of embedding information shouldn't distort query outputs too much. Recently, techniques have been proposed to watermark some classes of relational structures preserving first-order and monadic second order queries. For relational structures whose Gaifman graphs have bounded degree, watermarking can be done preserving first-order queries. We extend this line of work and study watermarking schemes for other classes of structures. We prove that for relational structures whose Gaifman graphs belong to a class of graphs that have locally bounded tree-width and is closed under minors, watermarking schemes exist that preserve first-order queries. We use previously known properties of logical formulas and graphs, and build on them with some technical work to make them work in our context. This constitutes a part of the first steps to understand the extent to which techniques from algorithm design and computational learning theory can be adapted for watermarking.

Cite as

Agnishom Chattopadhyay and M. Praveen. Query Preserving Watermarking Schemes for Locally Treelike Databases. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 36:1-36:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.FSTTCS.2019.36,
  author =	{Chattopadhyay, Agnishom and Praveen, M.},
  title =	{{Query Preserving Watermarking Schemes for Locally Treelike Databases}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{36:1--36:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.36},
  URN =		{urn:nbn:de:0030-drops-115988},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.36},
  annote =	{Keywords: Locally bounded tree-width, closure under minors, first-order queries, watermarking}
}
Document
Verification of Flat FIFO Systems

Authors: Alain Finkel and M. Praveen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.

Cite as

Alain Finkel and M. Praveen. Verification of Flat FIFO Systems. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.CONCUR.2019.12,
  author =	{Finkel, Alain and Praveen, M.},
  title =	{{Verification of Flat FIFO Systems}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.12},
  URN =		{urn:nbn:de:0030-drops-109147},
  doi =		{10.4230/LIPIcs.CONCUR.2019.12},
  annote =	{Keywords: Infinite state systems, FIFO, counters, flat systems, reachability, termination, complexity}
}
Document
Nesting Depth of Operators in Graph Database Queries: Expressiveness vs. Evaluation Complexity

Authors: M. Praveen and B. Srivathsan

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
Designing query languages for graph structured data is an active field of research, where expressiveness and efficient algorithms for query evaluation are conflicting goals. To better handle dynamically changing data, recent work has been done on designing query languages that can compare values stored in the graph database, without hard coding the values in the query. The main idea is to allow variables in the query and bind the variables to values when evaluating the query. For query languages that bind variables only once, query evaluation is usually NP-complete. There are query languages that allow binding inside the scope of Kleene star operators, which can themselves be in the scope of bindings and so on. Uncontrolled nesting of binding and iteration within one another results in query evaluation being PSPACE-complete. We define a way to syntactically control the nesting depth of iterated bindings, and study how this affects expressiveness and efficiency of query evaluation. The result is an infinite, syntactically defined hierarchy of expressions. We prove that the corresponding language hierarchy is strict. Given an expression in the hierarchy, we prove that it is undecidable to check if there is a language equivalent expression at lower levels. We prove that evaluating a query based on an expression at level i can be done in level i of the polynomial time hierarchy. Satisfiability of quantified Boolean formulas can be reduced to query evaluation; we study the relationship between alternations in Boolean quantifiers and the depth of nesting of iterated bindings.

Cite as

M. Praveen and B. Srivathsan. Nesting Depth of Operators in Graph Database Queries: Expressiveness vs. Evaluation Complexity. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 117:1-117:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{praveen_et_al:LIPIcs.ICALP.2016.117,
  author =	{Praveen, M. and Srivathsan, B.},
  title =	{{Nesting Depth of Operators in Graph Database Queries: Expressiveness vs. Evaluation Complexity}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{117:1--117:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.117},
  URN =		{urn:nbn:de:0030-drops-62520},
  doi =		{10.4230/LIPIcs.ICALP.2016.117},
  annote =	{Keywords: graphs with data, regular data path queries, expressiveness, query evaluation, complexity}
}
Document
Extending the Rackoff technique to Affine nets

Authors: Rémi Bonnet, Alain Finkel, and M. Praveen

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)


Abstract
We study the possibility of extending the Rackoff technique to Affine nets, which are Petri nets extended with affine functions. The Rackoff technique has been used for establishing EXPSPACE upper bounds for the coverability and boundedness problems for Petri nets. We show that this technique can be extended to strongly increasing Affine nets, obtaining better upper bounds compared to known results. The possible copies between places of a strongly increasing Affine net make this extension non-trivial. One cannot expect similar results for the entire class of Affine nets since coverability is Ackermann-hard and boundedness is undecidable. Moreover, it can be proved that model checking a logic expressing generalized coverability properties is undecidable for strongly increasing Affine nets, while it is known to be EXPSPACE-complete for Petri nets.

Cite as

Rémi Bonnet, Alain Finkel, and M. Praveen. Extending the Rackoff technique to Affine nets. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 301-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{bonnet_et_al:LIPIcs.FSTTCS.2012.301,
  author =	{Bonnet, R\'{e}mi and Finkel, Alain and Praveen, M.},
  title =	{{Extending the Rackoff technique to Affine nets}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{301--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.301},
  URN =		{urn:nbn:de:0030-drops-38688},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.301},
  annote =	{Keywords: Complexity of VASS, Affine nets, Rackoff technique, model checking, coverability, boundedness}
}
Document
Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE

Authors: M. Praveen and Kamal Lodaya

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)


Abstract
We consider concurrent systems that can be modelled as $1$-safe Petri nets communicating through a fixed set of buffers (modelled as unbounded places). We identify a parameter $\ben$, which we call ``benefit depth'', formed from the communication graph between the buffers. We show that for our system model, the coverability and boundedness problems can be solved in polynomial space assuming $\ben$ to be a fixed parameter, that is, the space requirement is $f(\ben)p(n)$, where $f$ is an exponential function and $p$ is a polynomial in the size of the input. We then obtain similar complexity bounds for modelchecking a logic based on such counting properties. This means that systems that have sparse communication patterns can be analyzed more efficiently than using previously known algorithms for general Petri nets.

Cite as

M. Praveen and Kamal Lodaya. Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 347-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{praveen_et_al:LIPIcs.FSTTCS.2009.2331,
  author =	{Praveen, M. and Lodaya, Kamal},
  title =	{{Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{347--358},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2331},
  URN =		{urn:nbn:de:0030-drops-23314},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2331},
  annote =	{Keywords: Petri nets, Coverability, Boundedness, paraPSPACE}
}
  • Refine by Author
  • 8 Praveen, M.
  • 2 Bhaskar, Ashwin
  • 2 Finkel, Alain
  • 1 Bilz, Raphael
  • 1 Bonnet, Rémi
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Verification by model checking
  • 1 Computing methodologies → Modeling and simulation
  • Show More...

  • Refine by Keyword
  • 2 complexity
  • 1 Affine nets
  • 1 Boundedness
  • 1 Büchi automata
  • 1 Complexity of VASS
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2019
  • 1 2009
  • 1 2012
  • 1 2016
  • 1 2020
  • 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