Семинары 2019-2020 уч.г.

29.06 Data and Reference Semantic-Based Simulator of DB-nets with the Use of Renew Too

Докладчик –Антон Ригин, студент 1 курса магистерской программы "Системная и программная инженерия" факультета компьютерных наук.

Аннотация. The complexity of the software and other systems is constantly growing, which is even more enhanced by concurrency of processes in the system, so modeling and validating of such systems is necessary in order to eliminate the failures. Because of the concurrency, traditional finite state machines (FSMs) are not sufficient for solving this problem regardless whether the FSM is deterministic or non-deterministic. One of the most well-known formalisms for solving this problem is the Petri net and its modifications such as the colored Petri net, the reference net and others. However, the Petri nets and their mentioned modifications do not support modeling of the persistent data usage in the system. The solution is db-net which is the formalism consisting of the three layers: the control layer which is represented by the modified colored Petri net, the data logic layer which is represented by queries for retrieving the persistent data and actions for updating (modifying) this data and the persistence layer which is represented by the relational database, its schema and constraints for keeping the persistent data in the consistent condition. However, software tools which can simulate the db-net formalism running are not available in public. In the seminar we will present the software simulator for db-nets which was developed by us. It is developed as a plugin for the Renew (the Reference Net Workshop) software tool which is built as a collection of plugins written in Java. This also allows to support the existing Renew’s reference semantics. The SQLite embeddable relational DBMS is used as a base tool for implementing the db-net’s persistence layer. During the meeting we will present the theoretical foundations and the architecture of the developed simulator as well as the working simulator itself.

17.06 Методы и инструменты повышения эффективности алгоритмов майнинга процессов

Докладчик – Сергей Шершаков, старший преподаватель факультета компьютерных наук, научный сотрудник НУЛ ПОИС.

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

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

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

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

22.05 Modeling and analysis of processes in protocol systems using Coloured Petri Nets: study case IEEE 802.16 standard

Speaker: Dr. Ana Morales Bezeira, Communications and Network Research Center (CICORE), Laboratory of Mobile Networks, Wireless and Distributed Systems, School of Computer Science, Faculty of Science, Universidad Central de Venezuela

The IEEE 802.16 standard is responsible for specifying and describing the air interface of Broadband Wireless Access Systems (BWA) point-multipoint fixed and mobile wireless metropolitan area network, and it is limited to the description of the Medium Access Control (MAC) and physical (PHY) layers. The MAC layer is further divided in three sub-layers: the Service Specific Converge Sublayer (CS), the MAC Common Part Sublayer (MAC CPS), and the Security Sublayer. The MAC CPS is connection- oriented, so some of its functions are related to a “connection management process”. The MAC CPS defines the service that is provided to a user (which is the MAC CS upper layer). In the IEEE 802.16 standard, the service specifications are defined using the notion of service primitives. Service primitives provide an abstract way to describe the interaction between the service user (MAC CS) and the service provider (MAC CPS) at the MAC protocol level. In our research, we have focused on the verification of the MAC CPS connection management process. 

In order to verify a protocol system such as the MAC CPS connection management process, its “protocol specification” and its “service specification” must be well defined and validated. We found that some parts of the MAC CPS connection management process regarding its protocol specification and its service specification are ambiguous, difficult to understand, and imprecise. Thus in this work, we followed a well-known protocol verification methodology proposed by Jonathan Billington, based on the formal comparison between the service and the protocol specifications using Colored Petri Nets (CPN) and Finite-State Automata (FSA). This methodology has been successfully applied in other protocol systems. For example, in the formal modeling and analysis of the Edge Router Discovery Protocol (ERDP) by Lars Kristensen and Fagerland, in the Wireless Application Protocol (WAP) by Steven Gordon and J. Billington, and in the Resource Reservation Protocol (RSVP) by Maria Villapol and J. Billington, among others. 

Based on Billington’s methodology, we conducted formal modeling and analysis of the MAC CPS connection management service and protocol specifications using CPNs. Then, the state space of each CPN model can be reduced to FSAs. This allow us to generate and compare the service and the protocol languages. Any resulting difference between these languages showcases some incongruence between the service specification and the protocol specification, for example, a service has not been correctly implemented by the protocol. 

Interestingly, as a contribution of our research, the comparison between the service and the protocol language using Billington’s methodology threw out several pitfalls of the service and protocol specification, for which we analyze how they can affect the protocol implementation. We conclude that the use of CPNs can improve the protocol and service specifications, and to provide a formal base for similar emerging protocol systems. 

06.05 Efficient equivalence checking technique for some classes of automata (Part 2)

Speaker: Vladimir A. Zakharov, Leading Research Fellow

In the first part of the talk (April 22) a new technique for designing polynomial time equivalence checking procedures for various classes of automata was presented. This approach reduces the equivalence problem to the solvability problem for certain types of systems of linear equations over the semirings of languages or transductions. The solvability of such systems can be detected by means of Gaussian variable elimination techniques based on some combinatorial properties of prefix-free regular languages. In the second part it will be shown how to apply this approach to the equivalence checking of deterministic 2-tape finite automata, deterministic biautomata, and deterministic stateless machines. In the end, some promising lines for further research on the advancement of this uniform equivalence checking technique will be discussed.

29.04 О проблеме конечной определимости многообразий, порождённых алгебрами вычислимых функций

Докладчик – Валерий Анатольевич Соколов, д.ф.-м.н. профессор, ЯрГУ

Rafael Robinson showed that all primitive recursive functions of one variable and only they can be obtained from two functions s(x) = x+1 and q(x) = x – []2 by using the operations of addition +, superposition * and iteration i. 

Julia Robinson proved that from the same two functions, using the operations of addition +, superposition * and operation -1 of the inversion of functions, we can obtain all general recursive functions (under a certain condition on the inversion operation) and all partially recursive functions. 

Based on these results, Academician Maltsev introduced the Rafael Robinson algebra of all unary primitive recursive functions and two Julia Robinson algebras: the algebra of all unary general recursive functions and the algebra of all unary partially recursive functions, and proposed to study the properties of these algebras, including the problem:  

find out whether a finite basis of identities exists in these algebras, i.e. are the corresponding varieties generated by these algebras finitely definable?

In the topic, we give a negative answer to this question. 

22.04 Efficient equivalence checking technique for some classes of automata

Speaker: Vladimir A. Zakharov, Leading Research Fellow

Finite transducers, two-tape automata, and biautomata are related computational models descended from the concept of Finite State Automaton. In these models an automaton controls two heads that read or write symbols on the tapes in one-way mode. The behaviors of these three types of automata show many common features, and it is surprising that the methods for analyzing the behavior of automata developed for one of these models do not find suitable utilization in other models. The aim the research is to develop a uniform technique for building
polynomial-time equivalence checking algorithms for some classes of automata (finite transducers, two-tape automata, biautomata, single-state push-down automata) which exhibit certain features of deterministic or unambiguous behavior. This new technique is based on some combinatorial properties of prefix-free regular languages, and reduces the equivalence checking of automata to solvability checking of certain systems of equation over the semirings of languages or
transductions. As it turned out, such a checking can be quite simply carried out by the variable elimination method.

05.03 High-level Petri net dynamic visualization. First step

Speaker: Yaroslav Kotylev, Research Assistant

Enterprise software systems are usually large and complex. They can have complicated architecture and millions of different states. It is difficult to imagine a process of designing new software system or analysis of developed system without various modeling techniques. Visual presentation of the software system structure and behavior provides possibilities, which can facilitate better analysis. Graphical notation of Petri net formalism is often used for software system description. An extension of Petri net is high-level Petri net formalism can be successfully used for the description of modular software system. 

We will discuss possible methods of dynamic visualization of high-level Petri nets, which describe software system from behavioral perspective.

20.02 Petri Net Transformations: Abstraction, Refinement, Morphisms. Part 2

Speaker: Роман Нестеров, Research Assistant, Postgraduate Student and Lecturer at the Faculty of Computer Science 

The second part of this talk will mainly cover properties of refinement transformations. 

The use of Petri net transformations makes the verification of concurrent systems easier. On the one hand, starting from a sophisticated model, one may apply reduction transformations that preserve properties of the initial model and verify necessary properties on a transformed abstract model. On the other hand, having a simple model, it is possible to apply refinement transformations that yield a more complicated model reflecting properties of an initial abstract model. Abstraction/refinement relations between Petri net models can be formalized in several ways, one of which is based on morphisms allowing to substitute places with subnets or to collapse subnets to a single place in Petri nets. This talk will present several abstraction/refinement transformations that helps to systematically construct these morphisms. We will discuss properties and limitations of the proposed transformations and how they are related to the transformations already existing in the literature.

13.02 Petri Net Transformations: Abstraction, Refinement, Morphisms

Speaker: Роман Нестеров, Research Assistant, Postgraduate Student and Lecturer at the Faculty of Computer Science 

The use of Petri net transformations makes the verification of concurrent systems easier. On the one hand, starting from a sophisticated model, one may apply reduction transformations that preserve properties of the initial model and verify necessary properties on a transformed abstract model. On the other hand, having a simple model, it is possible to apply refinement transformations that yield a more complicated model reflecting properties of an initial abstract model. Abstraction/refinement relations between Petri net models can be formalized in several ways, one of which is based on morphisms allowing to substitute places with subnets or to collapse subnets to a single place in Petri nets. This talk will present several abstraction/refinement transformations that helps to systematically construct these morphisms. We will discuss properties and limitations of the proposed transformations and how they are related to the transformations already existing in the literature.

26.12 An Approach for the Specification and Analysis of Business Processes

Speaker: Khalil Mecheraoui, University of Abdelhamid Mehri Constantine 2, Laboratory of Modelling and Implementation of Complex systems (MISC Lab), Constantine, Algeria

In order to enable enterprises to operate more effectively and efficiently, providing a high reliability of the specification and analysis of business processes is an active research subject. In this seminar, we first introduce an extension of Petri nets called HL-DToN that was proposed to deal with different aspects of business processes by supporting different perspectives. Next, we explain how we provided an HL-DToN semantics for BPEL. This latter is the most well known and used composition language which defines business processes by the orchestration of various partner interactions. Then, we explain the concept of maximality semantics. Maximality semantics expresses the true-concurrency in a natural way avoiding the state explosion problem. Actually, it has been proven necessary and sufficient for the action refinement and for action durations. Next, we focus on a novel approach to construct a hybrid formalism coated by maximality semantics. We abstract the reachable states of HL-DToN and relations among them. Reachable states are hybrid zones that consist of time information (durations, start-event intervals, and clocks) as well as markings (free and bound tokens distribution). We call the new formalism: Hybrid-Zone Graph based on Maximality Semantics (ZoM). Furthermore, two important properties, namely Home Marking and Reversibility, are distinguished for HL-DToN and verified using the low-level formalism ZoM. Finally, the seminar is concluded by discussing our view of applying conformance checking techniques on real event logs.

19.12 Автоматический вывод реляционных инвариантов для нелинейных систем дизъюнктов Хорна с ограничениями

Докладчик: Дмитрий Мордвинов, кафедра системного программирования СПбГУ, JetBrains Research

Индуктивные инварианты являются удобным инструментом доказательства корректности программ. В последнее время стали популярны подходы к автоматическому выводу индуктивных инвариантов как решений систем дизъюнктов Хорна с ограничениями. Однако довольно часто решения нелинейных систем (т.е. систем с правилами, содержащими в посылке более одного применения реляционных символов) оказываются невыразимы с помощью ограничений. В докладе было введено обобщение понятия индуктивного инварианта для нелинейных систем, которое частично решает эту проблему, а также рассмотрены методы эффективного автоматического вывода таких инвариантов. Будет было рассказано о работе Дмитрия по внедрению механизма вывода реляционных инвариантов в ядро решателя Z3.

14.11 Modelling, Enactment and Verification of Data-aware Processes

Speaker: Андрей Ривкин, postdoctoral researcher, KRDB Research Center for Knowledge and Data, Free University of Bozen-Bolzano.

Data and business processes are the two key pillars in modern enterprise systems.  While data are often regarded as the main driver of organisation decisions (for example, the decision to order 1000 laptops depends on the amount of money available), processes describe how business operations should be conducted (for example, first place correctly the laptop order, then provide the company’s billing address etc.). Although data and processes are two different entities, they are tightly connected. Quite often, business processes consume, manipulate, and generate data; they communicate with each other through shared databases. These interactions influence the performance of the company as whole, and often require additional treatment such as correctness checking and verification in order to assure that everything works as expected and avoid possibly costly failures once the processes will be effectively enacted. While there have been various foundational studies on "data-aware” business processes, the creation of suitable “models” and “verification techniques” for data-aware business processes has a long road ahead. In fact, contemporary data modelling approaches almost never mention how to manipulate them in a process, and likewise business process modelling approaches disregard which data to consider. On the implementation side, integrating data and processes is still a very time consuming, demanding and ad-hoc effort.

In this talk we advance the state of the art in data-aware business process management. We create a bridge between recent foundational frameworks for data-aware processes, and corresponding models that are closer to actual systems and implementations. We consequently devise a number of novel formalisms that gradually enrich the process dimension with data-related aspects. We then study their modelling, verification, and enactment, leading towards corresponding proof-of-concept implementations, which in turn paves the way towards a concrete impact into the enterprise dimension.

21.10 Основные подходы и принципы предметной области Software Process Mining

Докладчик: Семен Тихонов, стажер-исследователь лаборатории

В докладе была рассмотрена предметная область Software Process Mining и ее основные подходы и принципы. На основании анализа программного кода и трасс исполнения программного обеспечения могут быть выявлены архитектурная модель, позволяющая отслеживать взаимодействие между различными компонентами программы, и шаблоны проектирования (design patterns) программного обеспечения. Ссылаясь на диссертационное исследование, Семен рассказал о методах обнаружения компонентов и интерфейсов программ. С их помощью производится построение архитектурной модели программы в нотации иерархических сетей Петри. Эти подходы позволяют получить поведенческую модель программного продукта, к которой могут быть применены уже существующие подходы области Process Mining для дальнейшей аналитики и работы с моделями информационных систем.

23.09 Синтез супервизоров (Supervisor synthesis)

Вторая лекция Юрий Глебовича Карпова в рамках курса ""Модальные логики и многоагентные системы".

Был рассмотрен сравнительно новый метод построения системы управления, обеспечивающей координированное поведение нескольких процессов, специфицированных в виде дискретных систем переходов с конечным числом состояний, управляемых событиями. В рамках этого метода при задании группы дискретных процессов (роботов) и требований на их “правильную работу”, система управления, обеспечивающая такую правильную работу (супервизор), может быть автоматически синтезирована из спецификации. 

Метод впервые описан около 30 лет назад: P. Ramadge and W. M. Wonham, “The control of discrete event systems,” Proceedings of the IEEE, vol. 77, no. 1, pp. 81–98, 1989.

16.09 Модальные логики и многоагентные системы

Цикл семинаров 2019/2020 уч.г. открыл профессор Санкт-Петербурского Политехнического университета Юрий Глебович Карпов.
Профессор прочел вступительную лекцию курса "Модальные логики и многоагентные системы".

Основные концепции модальных логик могут быть представлены не только как теории рассуждений с модальностями, но и как «строительные леса» окружающего мира с его новой реальностью – многоагентными системами искусственного интеллекта (ИИ). Проблема разработки коллективов моральных агентов с контролируемым поведением становится центральной проблемой компьютерной науки Модальная логика с ее 'социальной' направленностью оказалась весьма удобным формализмом для решения многих проблем ИИ. Модальные логики становятся формальным базисом разработки коллективов автономных роботов с гарантированными свойствами поведения.

Сам курс читается в МИЭМ (Таллинская,34, аудитория 506) по вторникам с 16:40 до 19:30.