Solving coverability problems of petri nets by partial deduction

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Solving coverability problems of petri nets by partial deduction

Full text

Pdf (562 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming table of contents

Montreal, Quebec, Canada

Pages: 268 - 279

Year of Publication: 2000

ISBN:1-58113-265-4

Authors

Michael Leuschel	Department of Electronics and Computer Science, University of Southampton, Southampton SO17 1BJ, U.K.
Helko Lehmann	Department of Electronics and Computer Science, University of Southampton, Southampton SO17 1BJ, U.K.

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 15, Citation Count: 5

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/351268.351298 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.

	1	P. A. Abdulla , K. Cerans , B. Jonsson , Yih-Kuen Tsay, General decidability theorems for infinite-state systems, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.313, July 27-30, 1996
	2	María Alpuente , Moreno Falaschi , Germán Vidal, Partial evaluation of functional logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.768-844, July 1998 [doi>10.1145/291891.291896]
	3	Béatrice Bérard , Laurent Fribourg, Reachability Analysis of (Timed) Petri Nets Using Real Arithmetic, Proceedings of the 10th International Conference on Concurrency Theory, p.178-193, August 24-27, 1999
	4	Witold Charatonik , Andreas Podelski, Set-Based Analysis of Reactive Infinite-State Systems, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.358-375, March 28-April 04, 1998
	5	D. De Schreye, R. Gl? uck, J. J?rgensen, M. Leuschel, B. Martens, and M. H. S?rensen. Conjunctive partial deduction: Foundations, control, algorithms and experiments. The Journal of Logic Programming, 41(2 & 3):231{277, November 1999.
	6	Giorgio Delzanno , Andreas Podelski, Model Checking in CLP, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.223-239, March 22-28, 1999
	7	Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	8	Catherine Dufourd , Alain Finkel , Ph. Schnoebelen, Reset Nets Between Decidability and Undecidability, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.103-115, July 13-17, 1998
	9	E. A. Emerson , K. S. Namjoshi, On Model Checking for Non-Deterministic Infinite-State Systems, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.70, June 21-24, 1998
	10	J. Ezparza. Decidability ofmodel-checking for in~nite-state concurrent systems. Acta Informatica, 34:85{107, 1997.
	11	Alain Finkel, The Minimal Coverability Graph for Petri Nets, Papers from the 12th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1993, p.210-243, June 01, 1991
	12	Alain Finkel , Ph. Schnoebelen, Fundamental Structures in Well-Structured Infinite Transition Systems, Proceedings of the Third Latin American Symposium on Theoretical Informatics, p.102-118, April 20-24, 1998
	13	Laurent Fribourg, Constraint Logic Programming Applied to Model Checking, Selected papers from the 9th International Workshop on Logic Programming Synthesis and Transformation, p.30-41, September 22-24, 1999
	14	Robert Glück , Michael Leuschel, Abstraction-Based Partial Deduction for Solving Inverse Problems - A Transformational Approach to Software Verification, Proceedings of the Third International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.93-100, July 06-09, 1999
	15	Thomas A. Henzinger , Pei-Hsin Ho, HYTECH: The Cornell HYbrid TECHnology Tool, Hybrid Systems II, p.265-293, January 1995
	16	G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 2:326{336, 1952.
	17	Neil D. Jones, An introduction to partial evaluation, ACM Computing Surveys (CSUR), v.28 n.3, p.480-503, Sept. 1996 [doi>10.1145/243439.243447]
	18	Jesper Jørgensen , Michael Leuschel, Efficiently Generating Efficient Generating Extensions in Prolog, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.238-262, February 12-16, 1996
	19	R. M. Karp and R. E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3:147{195, 1969.
	20	J. B. Kruskal. Well-quasi ordering, the tree theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210{225, 1960.
	21	M. Leuschel. The ecce partial deduction system and the dppd library of benchmarks. Obtainable via http://www.cs.kuleuven.ac.be/~dtai, 1996.
	22	Michael Leuschel, Program specialisation and abstract interpretation reconciled, Proceedings of the 1998 joint international conference and symposium on Logic programming, p.220-234, August 1998, Manchester, United Kingdom
	23	Michael Leuschel, Logic Program Specialisation, Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School, p.155-188, June 29-July 10, 1998
	24	Michael Leuschel , Helko Lehmann, Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction, Proceedings of the First International Conference on Computational Logic, p.101-115, July 01, 2000
	25	Michael Leuschel , Bern Martens , Danny De Schreye, Controlling generalization and polyvariance in partial deduction of normal logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.208-258, Jan. 1998 [doi>10.1145/271510.271525]
	26	Michael Leuschel , Thierry Massart, Infinite State Model Checking by Abstract Interpretation and Program Specialisation, Selected papers from the 9th International Workshop on Logic Programming Synthesis and Transformation, p.62-81, September 22-24, 1999
	27	R. Lipton. The reachability problem and the boundedness problem for Petri nets are exponential-space hard. Conference on Petri Nets and Related Methods, M.I.T., July 1975.
	28	J. W. Lloyd , J. C. Shepherdson, Partial evaluation in logic programming, Journal of Logic Programming, v.11 n.3-4, p.217-242, Oct./Nov. 1991 [doi>10.1016/0743-1066(91)90027-M]
	29	K. Marriott, L. Naish, and J.-L. Lassez. Most speci~c logic programs. Annals of Mathematics and Arti~cial Intelligence, 1:303{338, 1990.
	30	E. W. Mayr. An algorithm for the general Petri net reachability problem. Siam Journal on Computing, 13:441{460, 1984.
	31	Faron Moller, Infinite Results, Proceedings of the 7th International Conference on Concurrency Theory, p.195-216, August 26-29, 1996
	32	C. Racko~. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223{231, Apr. 1978.
	33	Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Terrance Swift , David Scott Warren, Efficient Model Checking Using Tabled Resolution, Proceedings of the 9th International Conference on Computer Aided Verification, p.143-154, June 22-25, 1997
	34	Wolfgang Reisig, Petri nets: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
	35	John M. Rushby, Mechanized Formal Methods: Where Next?, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.48-51, September 20-24, 1999
	36	Morten Heine Sørensen, Convergence of Program Transformers in the Metric Space of Trees, Proceedings of the Mathematics of Program Construction, p.315-337, June 15-17, 1998
	37	M. H. S?rensen and R. Gl? uck. An algorithm of generalization in positive supercompilation. In J. W. Lloyd, editor, Proceedings of ILPS'95, pages 465{479, Portland, USA, December 1995. MIT Press.
	38	R. Valk and G. Vidal-Naquet. Petri nets and regular languages. Journal of Computer and System Sciences, 23(3):299{325, Dec. 1981.
	39	Pierre Wolper , Bernard Boigelot, Verifying Systems with Infinite but Regular State Spaces, Proceedings of the 10th International Conference on Computer Aided Verification, p.88-97, June 28-July 02, 1998

CITED BY 5

	Michael Leuschel, Homeomorphic embedding for online termination of symbolic methods, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	Berndt Farwer , Michael Leuschel, Model checking object petri nets in prolog, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.20-31, August 24-26, 2004, Verona, Italy
	Michael Leuschel , Dan Elphick , Mauricio Varea , Stephen-John Craig , Marc Fontaine, The Ecce and Logen partial evaluators and their web interfaces, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Michael Leuschel , Maurice Bruynooghe, Logic program specialisation through partial deduction: Control issues, Theory and Practice of Logic Programming, v.2 n.4-5, p.461-515, July 2002
	Michael Leuschel, Declarative programming for verification: lessons and outlook, Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, p.1-7, July 15-17, 2008, Valencia, Spain