A structural induction theorem for processes

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A structural induction theorem for processes

Full text

Pdf (955 KB)

Source

Annual ACM Symposium on Principles of Distributed Computing archive
Proceedings of the eighth annual ACM Symposium on Principles of distributed computing table of contents

Edmonton, Alberta, Canada

Pages: 239 - 247

Year of Publication: 1989

ISBN:0-89791-326-4

Authors

R. P. Kurshan	AT&T Bell Laboratories, Murray Hill, NJ
K. McMillan	Carnegie Mellon University, Pittsburgh, PA

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 41, Citation Count: 24

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/72981.72998 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	BCG86	E M Clarke , O Grumberg , M C Browne, Reasoning about networks with many identical finite-state processes, Proceedings of the fifth annual ACM symposium on Principles of distributed computing, p.240-248, August 11-13, 1986, Calgary, Alberta, Canada [doi>10.1145/10590.10611]
	GS	S.M. German and A. P. Sistla. Reasoning about systems with many processes. GTE Laboratories Inc., Waltham, Massachusetts.
	Hen88	Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
	HK88	Z. Har'El and R. P. Kurshan. Software for analysis of coordination. In Proc. Inter'nat. Conf. Syst. Sci. Eng., pages 382-385. Pergamon, 1988.
	Kur85	R. P. Kurshan. Modelling concurrent processes. In Symp. Applied Math., volume 31, pages 45-57. Amer. Math. Soe., 1985.
	Kur87	It. P. Kurshan. Reducibility in analysis of coordination. In LNCIS, volume 103, pages 19- 39. Springer-Verlag, 1987.
	Mil80	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	Wal88	D. Walker. Bisimulations and divergence in cos. In Third Annual Symposium on Logic in Computer Science, pages 186-192. COmputer Society Press, 1988.

CITED BY 24

	Steven M. German , A. Prasad Sistla, Reasoning about systems with many processes, Journal of the ACM (JACM), v.39 n.3, p.675-735, July 1992
	Massimiliano Chiodo , Thomas R. Shiple , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Automatic compositional minimization in CTL model checking, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.172-178, November 1992, Santa Clara, California, United States
	J.-K. Rho , F. Somenzi, Inductive verification of iterative systems, Proceedings of the 29th ACM/IEEE conference on Design automation, p.628-633, June 08-12, 1992, Anaheim, California, United States
	Aarti Gupta , Allan L. Fisher, Representation and symbolic manipulation of linearly inductive Boolean functions, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.192-199, November 07-11, 1993, Santa Clara, California, United States
	E. M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997
	E. Allen Emerson , Kedar S. Namjoshi, Reasoning about rings, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-94, January 23-25, 1995, San Francisco, California, United States
	David Lesens , Nicolas Halbwachs , Pascal Raymond, Automatic verification of parameterized linear networks of processes, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.346-357, January 15-17, 1997, Paris, France
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994
	Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
	Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Allen Emerson , Jai Srinivasan, A decidable temporal logic to reason about many processes, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.233-246, August 22-24, 1990, Quebec City, Quebec, Canada
	Parosh Aziz Abdulla , Bengt Jonsson, Model checking of systems with many identical timed processes, Theoretical Computer Science, v.290 n.1, p.241-264, 1 January 2003
	C. Norris Ip , David L. Dill, Verifying Systems with Replicated Components in Mur&b.phiv;, Formal Methods in System Design, v.14 n.3, p.273-310, May 1999
	Jianan Li , I. Suzuki , M. Yamashita, A New Structural Induction Theorem for Rings of Temporal Petri Nets, IEEE Transactions on Software Engineering, v.20 n.2, p.115-126, February 1994
	BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction, IEEE Transactions on Software Engineering, v.30 n.6, p.403-417, June 2004
	Jan Friso Groote , Jos van Wamel, The parallel composition of uniform processes with data, Theoretical Computer Science, v.266 n.1-2, p.631-652, 09/06/2001
	A. Miller , M. Calder , A. F. Donaldson, A template-based approach for the generation of abstractable and reducible models of featured networks, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.51 n.2, p.439-455, February, 2007
	Muffy Calder , Alice Miller, Feature interaction detection by pairwise analysis of LTL properties: a case study, Formal Methods in System Design, v.28 n.3, p.213-261, May 2006
	Danny Dolev, Century papers at the first quarter-century milestone, Proceedings of the twenty-fifth annual ACM symposium on Principles of distributed computing, p.3-4, July 23-26, 2006, Denver, Colorado, USA
	I. V. Konnov , V. A. Zakharov, An Approach to the Verification of Symmetric Parameterized Distributed Systems, Programming and Computing Software, v.31 n.5, p.225-236, September 2005
	Raúl Monroy , Alan Bundy , Ian Green, Planning Proofs of Equations in CCS, Automated Software Engineering, v.7 n.3, p.263-304, July 2000
	M. Calder , A. Miller, An automatic abstraction technique for verifying featured, parameterised systems, Theoretical Computer Science, v.404 n.3, p.235-255, September, 2008
	Raúl Monroy , Alan Bundy , Ian Green, On Process Equivalence = Equation Solving in CCS, Journal of Automated Reasoning, v.43 n.1, p.53-80, June 2009