Abstract
One-counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters. The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexity of two natural restrictions which imply decidability.
We show that trace inclusion between a OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial countervalues as part of the input. Secondly, we show that the the trace universality problem of nondeterministic OCN, which is equivalent to checking trace inclusion between a finite and a OCN-process, is Ackermann-complete.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abdulla, P.A., Cerans, K.: Simulation Is Decidable for One-Counter Nets. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 253–268. Springer, Heidelberg (1998)
Böhm, S., Göller, S., Jančar, P.: Equivalence of Deterministic One-Counter Automata is NL-complete. In: STOC, pp. 131–140 (2013)
Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic 10(3), 16:1–16:30 (2009)
Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma. In: LICS, pp. 269–278 (2011)
Higuchi, K., Wakatsuki, M., Tomita, E.: Some Properties of Deterministic Restricted One-Counter Automata. In: IEICE E79-D.8, pp. 914–924 (July 1996)
Hofman, P., Lasota, S., Mayr, R., Totzke, P.: Simulation Over Onecounter Nets is PSPACE-Complete. In: FSTTCS, pp. 515–526 (2013)
Hofman, P., Mayr, R., Totzke, P.: Decidability of Weak Simulation on One-Counter Nets. In: LICS, pp. 203–212 (2013)
Hofman, P., Totzke, P.: Trace Inclusion for One-Counter Nets Revisited. In: CoRR abs/1404.5157 (2014) (full version of this paper)
Jančar, P.: Equivalences of Pushdown Systems Are Hard. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 1–28. Springer, Heidelberg (2014)
Jančar, P.: Undecidability of Bisimilarity for Petri Nets and Some Related Problems. TCS 148(2), 281–301 (1995)
Jančar, P., Esparza, J., Moller, F.: Petri Nets and Regular Processes. J. Comput. Syst. Sci. 59(3), 476–503 (1999)
Jančar, P., Kučera, A., Moller, F.: Simulation and Bisimulation over One-Counter Processes. In: STACS, pp. 334–345 (2000)
Sénizergues, G.: L(A) = L(B)? ENTCS 9, 43 (1997)
Stirling, C.: Deciding DPDA Equivalence Is Primitive Recursive. In: ICALP, pp. 821–832 (2002)
Totzke, P.: Inclusion Problems for One-Counter Systems. PhD thesis. LFCS, University of Edinburgh (2014)
Valiant, L.: Decision Procedures for Families of Deterministic Pushdown Automata. PhD thesis. University of Warwick (1973)
Valiant, L., Paterson, M.S.: Deterministic One-Counter Automata. JCSS 10(3), 340–350 (1975)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Hofman, P., Totzke, P. (2014). Trace Inclusion for One-Counter Nets Revisited. In: Ouaknine, J., Potapov, I., Worrell, J. (eds) Reachability Problems. RP 2014. Lecture Notes in Computer Science, vol 8762. Springer, Cham. https://doi.org/10.1007/978-3-319-11439-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-11439-2_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11438-5
Online ISBN: 978-3-319-11439-2
eBook Packages: Computer ScienceComputer Science (R0)