- Alexander Rabinovich (Tel Aviv University, Israel): Ambiguity Hierarchy of Regular Infinite Tree Languages.
- Abstract: An automaton is unambiguous if for every input it has at most one accepting computation.
An automaton is k-ambiguous (for k>0) if for every input it has at most k accepting computations.
An automaton is boundedly ambiguous if there is k such that for every input it has at most k accepting computations.
An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations.
The degree of ambiguity of a regular language is defined in a natural way.
A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous)
automaton.
Over finite words every regular language is accepted by a deterministic automaton.
Over finite trees every regular language is accepted by an unambiguous automaton.
Over infinite-words every regular language is accepted by an unambiguous Buchi automaton
and by a deterministic parity automaton.
Over infinite trees Carayol et al. showed that there are ambiguous languages. We show that over infinite trees there is a hierarchy of degrees of ambiguity:
For every k>1 there are k-ambiguous languages which are not k-1 ambiguous; there are finitely (respectively countably, uncountably) ambiguous languages which are not boundedly (respectively finitely, countably) ambiguous.
- Борис Николаевич Карлов (Тверской государственный университет, Россия): (m,n)-жёсткие категориальные грамматики.
- Аннотация: Мы определяем (m,n)-жёсткие категориальные грамматики. Это классические категориальные грамматики, в которых категория каждого символа однозначно определяется его m левыми и n правыми соседями. Построен алгоритм, который по грамматике G и числам m, n определяет, является ли G (m,n)-жёсткой. Доказано, что в классе (m,n)-жёстких языков существует бесконечная иерархия, а также что класс (m,n)-жёстких языков несравним с классом регулярных языков. Исследуется сложность проблемы принадлежности для (m,n)-жёстких грамматик.
- Сергей Михайлович Дудаков (Тверской государственный университет, Россия): О неразрешимости теорий языков и их обобщений.
- Аннотация: Рассматриваются алгебры, элементами которых являются языки определенного вида (конечные, регулярные, все) в заданном алфавите. Над языками рассматриваются классические операции: объединение, конкатенация, итерация (замыкание Клини). Исследуется вопрос о разрешимости теории такой алгебры для разных наборов указанных операций. Установлено, что разрешимой теория будет только для одной операции объединения или для одной операции итерации. Во всех остальных случаях теория будет эквивалентной элементарной арифметике, то есть неразрешимой. Изучается вопрос обобщения этого результата на произвольные алгебры: переход от алгебры к алгебре подмножеств с теми же операциями. Найден пример, когда получаемая теория становится более простой. С другой стороны, для широкого класса коммутативных моноидов и, в частности, абелевых групп доказана неразрешимость теории подмножеств.
- Alex Dekhtyar (California Polytechnic State University, USA): Teaching Software Engineering for All Course (a joint talk with Bruno da Silva).
- Abstract: With every year more and more professionals with no computing education join the ranks of people who participate in various capacities in software development process in their companies. These people serve as Product Managers, Product Owners, subject matter experts, end users, quality assurance specialists, and in some other capacities. Yet, they start their participation in software development without the knowledge about the software development process that most professionals with Computer Science education get during their undergraduate study. To rectify this issue, we developed and piloted a new general education course "Software Engineering Without Programming" and taught this course during Winter 2020 quarter at Cal Poly to two sections of students from a wide range of degree objectives. In this presentation, we discuss the motivation for the course, its content, and will share our observations on the outcomes and lessons learned.
- Alexey Lisitsa (University of Liverpool, UK): Finite countermodel finding for the infinite-state and parameterized verification.
- Abstract: The set of first-order formulae valid in finite models in not r.e. as it was shown in the seminal paper by Prof B. A. Trakhtenbrot. The set of satisfiable
in finite formulas to the contrary is enumerable and there are efficient model building procedures, which given a formula return a finite model if it exists.
In this talk we overview a conceptually simple but powerful and efficient method for automated safety verification of infinite-state and parameterized systems.
The method is based on modelling of the system of interest in first-order predicate logic and verification via disproving by automated finite model building.
We report on relative completeness of the method wrt methods based on regular invariants and illustrate it by a few examples.
We discuss the challenges and formulate a few conjectures.
- Vladimir Sazonov (University of Liverpool, UK): From Sequential Computability to Naturally Continuous Non-dcpo Domains - informal description.
- Abstract: I will present here some informal description of my work around sequential computability from Novosibirsk 1974 to Liverpool 2015.
The aim is to introduce the main ideas in simple terms, avoiding technical details as much as possible.
- Sergei Artemov (Graduate Center CUNY, USA): On aggregating probabilistic evidence.
- Abstract: Imagine a database - a set of propositions Gamma = {F_1, ..., F_n} with some kind of probability estimates and let a proposition X logically follow from Gamma. What is the best justified lower bound of the probability of X? The traditional approach, e.g. within Adams' probability logic, computes the numeric lower bound for X corresponding to the worst-case scenario. We suggest a more flexible parameterized approach by assuming probability events u_1, u_2, ..., u_n that support Gamma and calculating aggregated evidence e(u_1, u_2,..., u_n) for X. The probability of e provides a tight lower bound for any, not only a worst-case, situation. The problem is formalized in a version of justification logic and the conclusions are supported by corresponding completeness theorems. This approach can handle conflicting and inconsistent data and allows the gathering both positive and negative evidence for the same proposition.
- Валерий Анатольевич Соколов (Ярославский Государственный Университет, Россия): Об одной проблеме в алгебрах вычислимых функций.
- Abstract: В 1947 году Рафаэль Робинсон показал, что все примитивно рекурсивные функции, зависящие от одного аргумента, и только они могут быть получены из двух функций s(х) = х + 1 и q(х) = х − [х]^2 с помощью операций сложения +, суперпозиции ∗ и итерации i.
В 1950 году Джулия Робинсон доказала, что из этих же двух функций с помощью операций сложения +, суперпозиции ∗ и операции −1 обращения функций можно получить все общерекурсивные функции (при определённом условии на операцию обращения) и все частично рекурсивные функции.
На основании этих результатов в 1961 году А. И. Мальцев ввёл в рассмотрение алгебру Рафаэля Робинсона всех одноместных примитивно рекурсивных функций и две алгебры Джулии Робинсон: частичную алгебру всех одноместных общерекурсивных функций и алгебру всех одноместных частично рекурсивных функций, и предложил исследовать свойства этих алгебр, в том числе, выяснить, существуют ли в этих алгебрах конечные базисы тождеств. Это явилось началом весьма широкого исследования в последующие годы целым рядом математиков свойств алгебр вычислимых функций. Однако, проблема существования (или невозможности существования) конечных базисов тождеств в алгебрах Р. Робинсона и Дж. Робинсон оставалась открытой.
В представленном нами докладе сообщается, что конечного базиса тождеств ни в одной из указанных алгебр не существует.
|
