IJPAM: Volume 115, No. 3 (2017)

Title

A MATHEMATICAL LOGIC VALIDATION PROCEDURE
FOR PETRI NETS MODELS

Authors

Zvi Retchkiman Königsberg
Instituto Politécnico Nacional, CIC
Mineria 17-2, Col. Escandon, Mexico D.F 11800, MEXICO

Abstract

A discrete event system, is a dynamical system whose state evolves in time by the occurrence of events at possibly irregular time intervals.. Place-transitions Petri nets, commonly called Petri nets, are a graphical and mathematical modeling tool applicable to discrete event systems in order to represent its states evolution.

This paper proposes a formal modeling and validation mathematical analysis methodology, which consists in representing the Petri net model of a discrete event system, by means of a formula in the propositional calculus logic. Then, using the concept of logic implication, and transforming this logical implication relation into a set of clauses, qualitative methods for validation are addressed.

History

Received: May 29, 2017
Revised: July 19, 2017
Published: July 27, 2017

AMS Classification, Key Words

AMS Subject Classification: 03B70, 93A30, 93D99, 93C10
Key Words and Phrases: Petri net models, discrete event systems, propositional logic, validation, refutation methods

Download Section

Download paper from here.
You will need Adobe Acrobat reader. For more information and free download of the reader, see the Adobe Acrobat website.

Bibliography

1
J.A. Robinson, A machine-oriented logic based on the resolution principle, Journal of the ACM, 12, No. 1 (1965), 23-41.

2
M. Davis, R. Sigal and E. Weyuker, Computability, Complexity, and Languages, Fundamentals of Theoretical Computer Science, Academic Press, 1983.

3
J. H. Gallier, Logic For Computer Science Automatic Theorem Proving, Dover, 2015.

How to Cite?

DOI: 10.12732/ijpam.v115i3.14 How to cite this paper?

Source:
International Journal of Pure and Applied Mathematics
ISSN printed version: 1311-8080
ISSN on-line version: 1314-3395
Year: 2017
Volume: 115
Issue: 3
Pages: 607 - 619


Google Scholar; DOI (International DOI Foundation); WorldCAT.

CC BY This work is licensed under the Creative Commons Attribution International License (CC BY).