автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Анализ семантических свойств некоторых классов программ и сетей Петри

Введение

1 Предварительные сведения

1.1 Мультимножества.

1.2 Квазиупорядоченные множества.

1.3 Системы помеченных переходов.

1.4 Сети Петри.

1.5 Сети Петри высокого уровня.

2 Вложенные сети Петри: двухуровневые системы

2.1 Сети Петри и моделирование мультиагентных систем

2.2 Начальные примеры.

2.3 Структура сети.

2.4 Поведение сети.

2.5 Вложенные сети Петри как вполне структурированные системы переходов.

2.6 Анализ семантических свойств.

3 Многоуровневые и рекурсивные вложенные сети Петри

3.1 Определение структуры и поведения.

3.2 Многоуровневые сети как вполне структурированные системы переходов.

3.3 Алгоритмы анализа для многоуровневых сетей.

3.4 Пример рекурсивной вложенной сети.

3.5 Вложенные сети с автономными и локализованными элементами.

3.6 Проблемы останова и поддержки активности переходов для рекурсивных сетей.

4 Сравнение вложенных сетей с другими формальными моделями

4.1 Языковая выразгггельность вложенных сетей Петри

4.2 Вложенные сети Петри и алгебры процессов.

4.3 Вложенные сети Петри и другие классы сетей Петри

4.4 Вложенные сети Петри и Линейная логика.

5 Семантика и доказательство некоторых свойств сетей Петри

5.1 Каузальная семантика для элементарных сетей Петри

5.2 Каузальная семантика для сетей позиций/переходов

5.3 Временная логика для доказательства свойств безопасности

5.4 Анализ поведения сетей высокого уровня.

5.5 Анализ поведения модульных сетей Петри.

6 Семантика и верификация последовательных программ

6.1 Хоаровская логика для функциональных программ.

6.2 Функциональные программы и присваивание.

6.3 Аксиоматическая семантика программ над абстрактными типами данных.

6.4 Процедурная реализация абстрактных типов данных

в настоящее время большое внимание уделяется разработке формализмов для анализа поведенческих свойств и верификации программных, аппаратных, технологических систем и процессов. Это обусловлено, с одной стороньк, быстрым ростом возможностей и усложнением компьютерных устройств, в частности, широким распространением параллельных и распределенных систем и, с другой стороны, очень высокой стоимостью ошибок, обнаруживаемых на поздних стадиях проектирования.

История становления теории формальных моделей вычислительных систем насчитывает уже более трех десятков лет и переживает в настоящее время бурное развитие в связи с появлением новых сетевых технологий. При этом большое внимание уделяется применению математических методов и, в частности, методов математической логики при описании семантики и анализе семантических свойств. Использование формальных моделей позволяет проводить предварительную симуляция и отладка программ и систем, а также применять математические методы для обоснования их правильности.

Особый интерес в этом направлении представляют исследования распределенных систем, характеризуемых отсутствием централизованного управления работой системы. Отдельные компоненты такой системы могут работать параллельно и независимо, взаимодействуя через общие переменные или обмен сообщениям. Одним из наиболее популярных формализмов для моделирования и анализа таких систем являются сети Петри. ПредлояЛенное К. Петри в бО-х годах сетевое представление распределенных систем активно развивается и в настоящее время. Среди отечественных иссяедований по сетям Петри, спецификации и анализу распределенных систем отметим работы H.A. Анисимова, О.Л. Бандман, И.М. Вир-бицкайте, Н.В. Евтушенко, Ю.Г. Карпова, В.Е. Котова, В.Н. Непомнящего, А. Петренко, P.M. Смслянского, В.А. Соколова, Л.А. Черкасовой.

Сети Петри характеризуются наглядностью и простотой сетевого представления, наличием четкой математической модели и разрешимостью многих важных поведенческих свойств, таких как проблемы останова, достижимости, покрытия, ограниченности, живости и др. Для решения практических задач и проектирования реальных сложных систем разработаны различные расширения формализма сетей Петри такие, как раскрашенные сети Петри К. Йен сена [78], временные сети Петри, сети Петри с ингибиторными дугами и др.

Некоторым недостатком сетей Петри является их слабая структурированность. Для облегчения процесса проектирования многие авторы расширяют аппарат сетей Петри за счет тех или иных конструкций модульности и иерархичности. При этом, как правило, структурирование производится на синтаксическом уровне, и структурная сеть путем определенных преобразований может быть преобразована в обыкновенную сеть Петри. Между тем, при моделировании реальных систем возникает потребность моделирования систем с динамической сетевой структурой. Примером таких систем являются мультиагентные системы, в которых агенты с автономным поведением могут появ,ляться, исчезать, копироваться и т.п. Поэтому в последнее время интерес многих исследователей (Р. Фальк [140], Л. Лакос [88] и др.) привлекает сочетание аппарата сетей Петри со средствами объектно-ориентированного подхода с целью получения структурированных моделей, явно отражающих иерархическую и мультиагентную структуру системы. В настоящее время также разрабатывается целый ряд программных систем, основанных на сетях Петри, и дополненных конструкциями объектно-ориентированного программирования, например, С00РК/2 [41], ОСоК [144], ООРКЬ [54] и др. При этом добавление тех или иных языковых конструкций производится, как правило, исходя из требований приложений без определения их формальной семантики. Таким образом, существует необходимость теоретического обоснования интеграции сетей Петри и объектно-ориентированного подхода, разработки соответствующего формализма, описания семантики новой модели, исследования возможностей ее анализа и сравнения с другими известными формализмами.

Цель работы состоит в разработке нового удобного формализма для проектирования поведения сложных мультиагентных систем, на основе сетей Петри и объектно-ориентированного подхода и в совершенствовании средств и методов описания математической семантики и доказательства семантических свойств последовательных и распредошенных программ и систем.

Достижение цели связывается с решением следующих задач:

• Разработать расширение формализма сетей Петри для .моделирования сложных мультиагентных систем за счет идей объектно-ориентированного подхода.

• Для разработанного формализма определить математическую семантику и исследовать разрешимость проблем останова, достижимости, покрытия, ограниченности и др. В случае разрешимости, разработать соответствуюш;ие алгоритмы.

• Сравнить выразительность разработанного формализма относительно других формальных моделей распределенных систем, в частности, относительно других расширений сетей Петри и алгебр процессов.

• Совершенствовать методы доказательства свойств сетей Петри на основе композиционального подхода.

• Исследовать вопросы семантики и доказательства правильности функциональных программ и программ над абстрактными типами данных.

Методы исследования, базируются на аппарате математической логики, теории квазипорядков и теории сетей Петри. В частности, при разработке методов анализа семантических свойств использовались теории программных и временных логик, семантики параллелизма, вполне структурированных систем помеченных переходов.

Научная новизна. В работе описан и исследован новый формализм для моделирования и анализа поведения сложных иерархических муль-тиагентных систем — вложенные сети Петри. Также получены новые результаты по анализу семантических свойств сетей Петри и некоторых классов последовательных программ.

Теоретическая и практическая значимость. Работа носит теоретический характер. Формализм вложенных сетей Петри может использоваться как теоретическая основа при разработке программных средств проектирования и анализа поведенческих свойств информационных, производственных и др. систем, основанных на комбинации объектно-ориентированного подхода и сетевого представления, в частности, для моделирования и анализа мультиагентных систем.

Структура работы Диссертация состоит из введения, шести глав, заключения и списка литературы.

Заключение в диссертации получены новые теоретические результаты в области математической семантики и доказательства семантических свойств программ и распределенных систем. Введен и исследован новый класс вложенных сетей Петри, содержащий средства для моделирования систем со сложной иерархической и объектной структурой. Эти результаты могут использоваться в качестве теоретической основы при разработке средств программной поддержки для моделирования, трансформации, верификации программных, информационных и других систем.

Перечислим основные научные результаты, полученные в диссертации :

1. Определен класс вложенных сетей Петри (МР-сетей), предназначенный для моделирования и анализа иерархических мультиагентных систем, включая многоуровневый и рекурсивный случаи.

2. Доказана разрешимость проблем останова, поддержки управляющего состояния, неизбежности, покрытия для многоуровневых КР-сетей. Построены алгоритмы проверки указанных свойств. Для рекурсивных КР-сетей с локализованными элементами построены алгоритмы проверки свойств останова и поддержки активности переходов. Доказана неразрешимость для МР-сетей проблем достижимости и ограниченности.

3. Проведено сравнение выразительности МР-сетей с другими расширениями сетей Петри. Доказано, что КР-сети строго сильнее обыкновенных сетей Петри и строго слабее универсальных вычислительных моделей. Исследована языковая выразительность МР-сетей. Проведено сравнение их с алгебрами процессов.

4. Для обыкновенных и модульных сетей Петри разработаны компо-зициональные методы доказательства утверждений линейной временной логики. Построена полная аксиоматика для доказательства свойств безопасности сетей Петри.

5. Для сете?! Петри с контактами определена и исследована каузальная семантика.

6. Для функциональных программ, дополненных оператором присваивания, построены полная Хоаровская логика и система эквивалентных преобразований, элиминирующих присваивание.

7. Для программ над абстрактными типами данных (АТД) построена полная аксиоматическая семантика, не допускающая побочных эффектов и определена корректность процедурной реализации АТД, поддерживающая пошаговую разработку программ.

1. Агафонов В.Н. Типы и абстракция данных в языках программирования. М.: Мир, 1982. С. 265-327.

2. Анисимов H.A. Алгебра структур протоколов на основе теории сетей Петри // Автоматика и вычислительная техника, №1, 1987. С. 9-15.

3. Анисимов H.A. Рекурсивное определение протоколов на основе теории сетей Петри // Автоматика и вычислительная техника, №5, 1987. С. 3-7.

4. Анисимов H.A. Формальная модель для разработки и описания протоколов на основе теории сетей Петри // Автоматика и вычислительная техника, Дбб, 1988. С. 3-10.

5. Бандман M.R. и др. Территориально-производственные комплекал: Прогнозирование процесса формирования с использованием сетей Петри. Новосибирск: Наука. Сиб. отд-ние, 1990.

6. Котов В.Е. Сети Петри. М.: Наука, 1984.

7. Куратовский К., Мостовский А. Тория множеств. М.: Мир, 1970.

8. И. Курош А.Г. Лекции по общей алгебре. М.: Наука, 1973.

9. Ломазова И.А. О сложности индуктивных условий для верификации арифметических программ // Материалы Всес. Студенческой конференции "Студент и научно-технический прогресс", Новосибирск, 1978. С. 85-94.

10. Ломазова И.А. Хоаровская логика для функциональных программ // Проблемы системного л теоретического программирования. Новосибирск: НГУ, 1984. С. 148-156.

11. Ломазова И.А. Редуцирующие преобразования для функциональных программ с присваиванием // Программирование, №3, 1986. С. 1724.

12. Ломазова И.А. Аксиоматическая семантика программ, не допускающая побочных эффектов // Прикладная логика (Вычислительные системы, вып. 116). Новосибирск, 1986. С. 129-137.

13. Ломазова И.А. Пошаговая разработка корректных программ посредством процедурной реализации абстрактных типов данных // Новые методы конструирования программ. Новосибирск: НГУ, 1986. С. 74-83.

14. Ломазова И.А. Моделирование мультиагентных динамических систем вложенными сетями Петри // Программные системы: Теоретические основы и приложения. — М.: Наука. Физматлит, 1999. С. 143-156.

15. Ломазова И.А. Каузальная семантика для сетей Петри с контактами // Программирование, №4, 1999. С. 214-221.

16. Ломазова И.А. Некоторые алгоритмы анализа для многоуровневых вложенных сетей Петри // Известия РАИ. Теория и системы управления, №6, 2000. С. 965-974.

17. Ломазова И.А. Рекурсивные в.ложенные сети Петри: анализ семантических свойств и выразительность // принято к публикации в ж. Программирование, 2001.

18. Ломазова И.А., Лысенко Н.В. Моделирование задачи разделенного доступа средствами модульных сетей Петри // Моделирование и анализ информационных систем. Вып. 5. Ярославль: Ярославский госуниверситет, 1998. С. 62-73.

19. Непомнящий В.А. Практические методы верификации программ // Кибернетика, JYo2, 1984. С. 21-28, 43.

20. Хендерсон П. Функциональное программирование. Применение и реализация. М.: Мир, 1983.

21. Agerwaia Т., Flinn М. Comments on capabilities, Umitaions and "correctness" of Petri net // Proc. of the 1st Annual Symposium on Computer Architecture. New York, 1973. P. 81-86.

22. Abdulla P.A., Cerans K., Jonsson В., and Yih-Kuen T. General decidabihty theorems for infinite-state systems // Proc. 11th IEEE Symp. Logic in Computer Science (LICS'96), New Brunswick, N.J, USA, July 1996, 1996. P. 313-321.

23. Anisimov, N., Kovalenko, A. Asynchronous Composition of Petri Nets via Places // Perspectives of System Informatics (Proceedings of the Andrei Ershov Second International Alemorial Conference). Novosibirsk, 1996, P. 214-219.

24. Apt K.R. Ten years of Hoare's logic: A survey Part 1 // ACM Trans. Progr. Lang. Syst., vol. 3, №4, 1981. P. 431-483.

25. Araki T. and Kasami Т. Some decision problems related to the reachability problem for Petri nets // Theoretical Computer Science, 3(1), 1977. P. 85-104

26. Bacus J. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs // Comm. ACM 21(8), 1978. P. 613-641.

27. Badouel E. Réseaux de Petri à structures dynamiques, une bibliographie commentée // Modélisation et vérification des processus parallèles (MOVEP'98), Actes de l'école d'été, École Centrale de Nantes, 6-9 Juillet 1998. P. 201-206.

28. Baeten J.C.M., Bergstra J.A. and Klop J.W. Decidability of bisimulation equivalence for processes generating context free languages // Lecture Notes in Computer Science 259, Springer-Verlag, 1987.

29. Battistou E., Cindio F.D., Mauri G. OBJSA nets: a class of high-level nets having objects as domains // LNCS 340. Springer, 1988. P. 20-43.

30. Battiston E., Chizzoni A., De Cindio F. Inheritance and Concurrency in CLOWN // Proc. of the 2nd Workshop on Object-Oriented Programming and Models of Concurrency, Turin, 1995.

31. Bergstra J. A., Tucker J.V. The axiomatic semantics of programs based on Hoare's logic // Acta Informática, vol. 21, №3, 1984. P. 293-320.

32. Best E. Semantics of sequential and parallel programs. Prentice Hall, 1996.

33. Best E., DeviUers R. Sequential and concurrent behaviour in Petri net theory // Theoretical Computer Science, vol. 55, 1987. P. 87-136.

34. Best, E., Esparza, J. Model Checking of Persisitent Petri Nets // CSL'91, LNCS 626. Springer, 1992. P. 15-34.

35. Biberstein 0., Buchs B. An object-oriented specification language based on hierarchical algebraic Petri nets // Proc. of the IS-CORE Workshop, AMsterdam, September, 1994. Tech. Rep.EPFL-DI 94-76, 1994.

36. Biberstein 0., Buchs B., and Guelfi N. Modeling of cooperative editors usiing COOPN/2 // Proc. of the Int. Workshop on Object-Oriented Programming and Models of Concurrency, Osaka, Japan, June, 1996.

37. Blume E.K., Parisi-Presicce E. Implementation of data types by algebraic methods / /J. Comput. and Syst. ScL, vol. 27, №2, 1983. P. 304-330.

38. Brown C. Relating Petri nets to formulae of Linear logic. Technical report, Department of Computer Science, University of Edinburgh, 1989.

39. Cherkasova L.A., Kotov V.E. Structured nets // Proc. of the 6th

40. MFCS, LNCS 118. Springer-Verlag, 1981. P. 242-251.

41. Christensen S. Decidability and decomposition in Process Algebra. PhD thesis. University of Edinburgh, 1993.

42. Christensen S. Petrucci L. Towards a Modular Analysis of Coloured Petri Nets // Proc. Int. Conf. on Applications and Theory of Petri Nets, LNCS 616. Springer-Verlag, 1992. P. 113-133.

43. Ciardo G. Petri nets with marking-dependent arc cardinality: Properties and analysis // Proc. 15th Int. Conf. Application and Theory of Petri Nets, Zaragoza, Spain, June 1994, LNCS 815. Springer,1994. P. 179-198.

44. Cook S.A. Soundness and completeness of an axiomatic system for program verification // SIAM J. Computing, vol. 7, 1978. P. 70-90.

45. Dershowitz N., Jouannaud J.-P. Rewrite systems // Chapter 6 of the Handbook of Theoretical Computer Science B:Formal Aiethods and Themantics, J. van Leeuwen, ed. North-Holland, Amsterdam, 1990. P. 243-320.

46. Dershowitz N., Manna Z. Proving termination with multiset orderings // Communications of the A C M , 22(8), 1979. P. 465-476

47. Diekert V., Rozenberg G. (Eds.) The book of traces. World Scientific,1995.

48. Dufourd C, Einkel A., and Schnoebelen Ph. Reset nets between decidability and undecidability // Proc. 25th Int. Coll. Automata, Languages, and Programming (ICALP'98), LNCS 1443. Springer, 1998. P. 103-115.

49. Ehrig H., Kreowski H.-J., Padawit Z.P. Algebraic implementation of abstract data types: Concept, syntax, semantics and correctness // Lecture Notes in Computer Science, vol. 85, 1980. P. 142-153.

50. Eehling R. A concept of hierarchical Petri nets with building blocks // G. Rozenberg (Ed.) Advances in Petri nets, LNCS 674. Springer, 1993. P. 148-168.

51. Earwer B. A Linear Logic view of object Petri nets // Fundamenta Informática, vol. 37, №3, 1999. P. 225-246.

52. Earwer B. A multi-region Linear Logic based calculus for dynamic Petri net structure // Fundamenta Informaticae, vol. 43, Aol-4, 2000. P. 6179.

53. Farwer B. Linear logic based calculi for object Petri nets. Dissertation. Logos Verlag, ISBN 3-89722-539-5, Berlin, 2000.

54. Finkel A. Reduction and covering of infinite reachability trees // Information and Computation, 89(2), 1990. P. 144-179

55. Finkel A.and Ph. Schnoebelen Ph. Well-structured transition systems everywhere! // Theoretical Computer Science, 256(1-2), 2001. P. 6392.

56. Finkel A.and Ph.A Schnoebelen Ph. Fundamental structures in weU-structurecl infinite transition systems // Proc. 3rd Latin American Theoretical Informatics Symposium (LATIN'98), Campinas, Brazil, Apr. 1998, LNCS 1380. Springer, 1998. P. 102-118.

57. Floyd, R. Assigning meaning to program // J.T.Schwartz (ed.) Proc. of Symposium on Applied Mathematics 19, Mathematical Aspects of Computer Science, American Mathematical Society, New York, 1967. R 19-32.

58. H.Genrich, K.Lautenbach. System modeling with high-level Petri nets // Theoretical Computer Science, 13, 1981. P. 109-136

59. H.Genrich. Equivalence transformations of PrT-nets // Advances in Petri nets 1989, LNCS 424. Springer-Verlag, 1990. P. 179-208.

60. Girard J.-Y. Linear Logic // Theoretical Computer Science, vol. 50, 1987. P. 1-102.

61. Goltz U., Reisig W. The non-sequential behaviour of Petri nets // Information and Control, vol. 57, №2-3. 1983. P. 125-147.

62. Haddad S., Poitrenand D, Theoretical aspects of recursive Petri nets // Proc. ATPN'99, LNCS 1639. Springer, 1999. P. 228-247.

63. Higman G. Ordering by divisibihty in Abstract Algebra // Proc. London Math. Soc, 3(2), 1952. P. 326-336.

64. Hoare, C.A.R. An Axiomatic Basis for Computer Programming // Communications ACM, vol. 12, №10, 1969. P. 576-580.

65. Hoare C.A.R. Proof of correctness of data representations // Acta Informfnica, vol. 1, 1972. P. 271-281.

66. Holvoet T. Agents and Petri Nets // Petri Nets Newsletter, vol. 49, Gessellschaft für Informatik, Bonn, 1995. P. 3-8.

67. Hoogers P.W., Kleijn H.C.M., Thiagarajan P.S. An Event Structure Semantics for General Petri Nets // Theoretical Computer Science, vol. 153, 1996. P. 129-170.

68. Hong J.E. and Bae D.H. HOONets: Hierarchical Object-Oriented Petri Net for SYstem Modeling and Analysis // TR CS-TR-98-132, http://cs.kaist.ac.kr/library/tr/

69. T6. Jantzen M. Language Theory of Petri Nets // LNCS 254, Springer, 1987.

70. Jensen K. Coloured Petri nets and the invariant method // Theoretical Computer Science, vol. 14, 1981. P. 317-336.

71. Jensen K. Coloured Petri Nets. Vol.1. Eatcs Monographs on TCS, Springer-Verlag, 1994.

72. Keller R.AI. Vector replacement systems: a formalism for modelling asynchronous systems // Tech. Report 117, Princeton University, 1972.

73. Keller R.AI. Formal verification of parallel programs // Communications of the ACM, vol. 1, .№7. 1976. P.371-384.

74. Kindler E. A Compositional Partial Order Semantics for Petri Net Components // Technical Report TR 342/06/96 A, Technische Universität München, March 1996.

75. Kindler, E., Walter, R. Message Passing Mutex // J. Desel (Ed.): Structures in Concurrency Theory, Proceedings, Workshops in Computing, Springer, 1995.

76. Kosaraju S.R. Limitations of Dijkstra's semaphore, primitives and Petri nets // Operating Systems Review, vol. 7, №4, 1973. P. 122136.

77. Kozarju S.R. Decidability of reachability in vector addition systems // 14 Annual ACM Symp. on Theory of Computing, San-Francisko, 1982. R 267-281.

78. Kruskal J.B. Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture // Trans. Amer. Math. Soc. 95, 1960. P. 210-225.

79. Lamport L., Lynch N. Distributed Computing: Models and Methods / / J . van Leeuwen (ed.) Handbook of Theoretical Computer Science, Elsevier Science Publ. Co., 1990.

80. Lautenbach, К. Linear Algebraic Technique for Place/Transition Nets // W.Brauer, W.Reisig and G.Rosenberg (eds.): Petri Nets: Central Models and Their Properties, LNCS 254. Springer, 1987. P. 142-167.

81. Liu H., Park J.-C, Miller R.E. On Hybrid Synthesis for Hierarchical Structured Petri Nets // Technical Report CS-TR-3628, University of Maryland, Colledge Park, 1996.

82. Lomazova, I. A Complete Axiomatics for Proving Safety Properties of Petri Nets // Perspectives of System Informatics (Proceedings of the Andrei Ersliov Second International Memorial Conference). Novosibirsk, 1996. P. 268-272.

83. Lomazova LA. On occurrence net semantics for Petri nets with contacts // Proc. of 11th International Symposium on Eundamentals of Computation Theory LNCS 1279. Springer, 1997. P. 315-328.

84. Lomazova LA. Multi-Agent Systems and Petri Nets // Proc. of Int. Workshop "Distributed Artificial InteUigence and Alulti-Agent Systems" DAIMAS'97, June 15-18, 1997. St.Petersburg, 1997. P. 147152.

85. Lomazova LA. On Proving Large Distributed Systems: Petri Net Modules Verification // Proc. of the 4th Int. Conference on Parallel Computing Technologies, LNCS 1277. Springer-Verlag, 1997. P. 70-75.

86. Lomazova I.A., Schnoebelen Ph. Some Decidability Results for Nested Petri Nets // Perspectives of System Informatics (Proc. of Andrei Ershov Third International Conference). Novosibirsk: A.P.Ershov Institute of Informatics Systems, 1999. P. 143-148.

87. Lomazova LA. and Schnoebelen Ph. Some Decidabihty Results for Nested Petri Nets // Proc. Andrei Ershov 3rd Int. Conf Perspectives of System Informatics (РЗГ99), Novosibirsk, Russia, Jul. 1999, LNCS 1755. Springer-Verlag, 2000. P. 207-219.

88. Lomazova LA. Nested Petri nets — a formalism for specification of multi-agent distributed systems // Proc. of the Concurrency, Specification and Programming (CS&P'99) Workshop, Warsaw, Poland, 28-30 September 1999. Warsaw, 1999. P. 127-140.

89. Lomazova LA. Nested Petri nets for intelligent control design // Труды 4-го международного семинара по прикладной семиотике, семиотическому и интеллектуальному управлению ASC/IC'99, 18-20 октября 1999 г., Зеленоград. — М., ПАИМС, 1999. С. 102-111.

90. Lomazova I.A. Nested Petri nets — a Formalism for Specification and Verification of Multi-Agent Distributed Systems // Fundamenta Informaticae, vol.43, №1-4, 2000. P. 195-214.

91. Maibaum T.S.E., Veloso P.A.S., Sadler M.R. A theory of abstract data types for program development: bridging the gap? // Lecture Notes in Computer Science, vol. 186, 1985. P. 214-230.

92. Manna, Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.

93. Marti-Ohet N., Meseguer J. From Petri nets to Linear logic. Technical report, SRI International, Computer Science Laboratory, Stanford, 1989.

94. Mayr E.W. An Algorithm for the General Petri Net Reachability Problem // SIAM Journal on Computing, 1984, V. 13. P. 441-460.

95. Mellies P.-A. On a duality between Kruskal and Dershowitz theorem // Proc. of the 25th Int. Colloquium on Automata, Languages and Programming, Aaborg, 1998 (ICALP'98).

96. Milner R. A calculus of communicating systems // LNCS 92. Springer, 1980.

97. Milner R. Communication and concurrency. Prentice Hall Int., 1989.

98. Moldt D., Wienberg E. Multi-Agent Systems Based on Coloured Petri nets // Proc. Int. ConL on Application and Theory of Petri Nets, LNCS 1248. Springer-Verlag, 1997. R 82-101.

99. Nash-WiUiams, C.St.J.A. On well-quasi-ordering finite trees // Proc. of the Cambridge Philosophical Society 59(4), 1963. P. 833-835.

100. Nielsen M., Plotkin G., Winskel G. Petri nets, event structures and domains // Theoretical Computer Science, vol. 13, №1, 1981. P. 85108.

101. Nielsen M., Rozenberg G., Thiagarajan P.S. Behavioural notions for elementary net systems // Distributed Computing, vol. 4, №1, 1990. P. 45-57.

102. Park D.S.M. Concurrency and automata on infinite sequences // LNCS 104. Springer, 1981.

103. Perkusich A., Figueiredo J.CA. G-nets: A Petri nets based approach for logical and timing analyiys of complex software systems // J. of Systems and Software, vol. 39, 1997. P. 39-59.

104. Peterson, G. Myths about the mutual exclusion problem // Information Processing Letters, 12(3), 1981. P. 115-116

105. C.A.Petri. Kommunikation mit Automaten // PhD thesis. Institute für Instrumentelle Mathematik, Bonn, Germany, 1962.

106. Petri CA. Communication with automata // Rome Air Dev.Center, New York. Technical Report RADC-TR-65-377, 1966.

107. Petri C A . Concepts of net theory // Proeedings of the Symposium and Summer School Mathematical Foundations of Computer Science, 1973. P. 137-146.

108. Petri CA. Nonsequential processes // Gesellschaft fur Mathematik und Datenverarbeirtung, St.Augustin. Internal Report GMD-ISF-77-5, 1977.

109. Plotkin G. A structural approach to operational semantics // Diami FN-19, Computer Science Department, Aarhus University, 1981.

110. Reinhardt K. Reachabihty in Petri nets with inhibitor arcs // Unpublished manuscript. www-fs. Informatik, uni-tuenbingen.de/reiuhard, 1995 /

111. Reisig W. Petri nets. SpringerAAerlag, 1985.

112. Reisig W. Petri Nets in Software Engineering // Advances in Petri Nets 1986 Part 2, LNCS 255. Spinger-Verlag, 1987. P. 63-96.

113. Reisig W. Petri nets and algebraic specifications // Theoretical Computer Science, vol.80, 1991. P. 1-34.

114. Reisig, W. Elements of Temporal Logic Coping with Concurrency // TR 342/23/92, München: Technische Universität, Institut für Informatik, 1992.

115. Reisig W. Petri net models of distributed algorithms // LNCS 1000. Springer, 1995.

116. Robinson L., Levitt K.N. Proof techniques for hierarchially structured programs // Commun. ACM, vol. 2, №4, 1977. P. 271-283.

117. Rozenberg G., Thiagarajan P.S. Petri nets: basic notions, structure, behavior // Current Trends in Concurrency. Lecture Notes in Computer Science, vol. 224, 1986. P. 585-668.

118. Sibertin-Blanc C. Cooperative nets // Proc. of the 15th Int. Conf on Apphcation and Theory of Petri Nets, LNCS 815, Springer, 1994. P .471-490.

119. Smith E. On the border of causality: contacts and confusion // Theoretical Computer

120. Science, vol. 153, 1996. P. 245-270.

121. Smith, E. A SurA'ey on High-Level Petri-Net Theory // Bulletin

122. EATCS, vol. 59, 1996. P. 267-293.

123. Smith E. Principles of high-level net theory. Lectures on Petri nets // LNCS, 1491. Springer, 1998. R 174-210.

124. Thiagarajan P.S. Elementary net systems // LNCS 254. Springer, 1987. R 26-59.

125. Tuominen, H. Elementary Net Systems and Dynamic Logic //

126. G. Rosenberg (ed.): Advances in Petri Nets 1989, LNCS 424. Springer, 1990. P. 453-466.

127. Valk R. How to Define Markings in Object Systems // Petri Nets Newsletter, vol. 50, Gessellschaft fur Informatik, Bonn, 1995. P. 3-8.

128. Valk R. Petri Nets as Token Objects: An Introduction to Elementary Object Nets // Proc. Int. ConL on Application and Theory of Petri Nets, LNCS 1420. Springer, 1998. pp.1-25.

129. Valk R. Reference and value semantics for object Petri nets //

130. H. Weber, H.Ehrig, and W.Reisig (eds.) Coloquium on Petri Net Technologies for Alodelling Communication Based Systems. Eraunhofer Institute for Software and System Engeneering ISST, Berlin, 1999. P. 169-188.

131. Winkowski J. Event structure representation of the behaviour of place/transition systems // Fundamenta Informática, vol. 11, 1988. R 405-432.

132. Wirsing M., Broy M. An analysys of semantic models for algebraic specifications // Tlieor. Found. Program. Methodol. Lect. Not. Int. Summer School. Dordrecht e. a., 1982. R 351-413.

133. Wirtz G., Graf J., and Giese 11. Ruling the behaviour of distributed software components // Proc. Int. Conf on Parallel and Distributed Processing Techniques and Applications (PDPTA'97), Las Vegas, Nevada, July 1997.

134. Wooldridge M.J., Jennings N.R. Agent Theories, Architectures, and Languages: A Survey // Intelligent Agents. Proc. ECAI-94 Workshop on Agents Theories, Architectures, and Languages. Amsterdam, The Nehterlands, August 8-9, J994. Springer-Verlag, 1995.

135. Wulf W. A., London R.L., Sliaw M. .A.n introduction to the construction and verification of Alfard programs // IEEE Trans. Software Eng., SE-2, №4, 1976. P. 253-264.

136. Zapf M., Heinzl A. Techniques for integrating Petri nets and object-oriented concepts // Worlving Papers in Information Systems, №1, 1998. University of Bayreuth, 1998.