• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

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

Время/место проведения семинара. Регистрация внешних слушателей

Семинар проводится по адресу Покровский бульвар, 11.

Точную дату и время проведения можно посмотреть на главной странице лаборатории.

Студентам, преподавателям и сотрудникам вход свободный.
Для заказа разовых пропусков просьба обращаться к менеджеру лаборатории Жеребцовой Ксении по адресу kzherebczova@hse.ru

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. 


 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!
Сервис предназначен только для отправки сообщений об орфографических и пунктуационных ошибках.