Abstract
Pratt [13] introduced POMSETs (partially ordered multisets) in order to describe and analyze concurrent systems. A POMSET P gives a set of temporal constraints that any correct execution of a given concurrent system must satisfy. Let L(P) (the language of P) denote the set of all system executions that satisfy the constraints given by P. We show the following for finite POMSETs P, Q, and system execution x.
-
•
The POMSET Language Membership Problem (given x and P, is x ε L(P)?) is NP-complete.
-
•
The POMSET Language Containment Problem (given P and Q, is L(P) ⊑L(Q)?) is II2 p-complete.
-
•
The POMSET Language Equality Problem (given P and Q, is L(P) = L(Q)7) is at least as hard as the graph-isomorphism problem.
-
•
The POMSET Language Size Problem (given P, how many x are in L(P)?) is span-P-complete.
Because of space limitations, some of the results in this extended abstract are stated without proof. All proofs are given in the journal version of the paper, which is available in preprint form from the first author.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Aggarwal, R. P. Kurshan, and K. K. Sabnani. Protocol Specification, Testing and Verification III (1983), 19–34.
M. C. Brown, E. M. Clarke, and O. Grumberg. Inf. and Comput. 81:13–31, 1989.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. LICS '90, 428–439.
O. Coudert, C. Berthet, and J. C. Madre. Springer Verlag LNCS 407, 1989, 365–373.
D. L. Dill. Springer Verlag LNCS 407, 1989, 197–212.
M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979.
P. Godefroid. DIMACS Series, vol. 3, 1991, 321–340.
J. Kilian. Private communication.
J. Köbler, U. Schöning, and J. Toran. Acta Informatica 26:363–379, 1989.
R. P. Kurshan. Springer Verlag LNCS 430, 1990, 414–453.
R. P. Kurshan. Springer Verlag LNCIS 103, 1987, 19–39.
R. P. Kurshan and K. L. McMillan. PODC '89, 239–247.
V. Pratt. Intl. J. Parallel Programming 15(1):33–71, 1986.
D. Probst and H. Li. DIMACS Series, vol. 3, 1991, 15–24.
A. P. Sistla, M. Y. Vardi, and P. Wolper. Theor. Comput. Sci. 49:217–237, 1987.
H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing Language Containment for Ω-Automata using BDD's, Formal Methods in VLSI Design (1991), ACM, to appear.
L. Valiant. Theor. Comput. Sci. 8:189–201, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Feigenbaum, J., Kahn, J.A., Lund, C. (1992). Complexity results for POMSET languages. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_33
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive