semináre v roku 2018

2. 3. 2018, 11:00

Rasťo Královič

(KI FMFI UK)

   Konečné automaty s radou II.

Model neuniformných konečných automatov (a.k.a. automaty s radou) bol už na seminári pred časom prezentovaný. V prednáške predstavíme niekoľko nových výsledkov a otvorených problémov, ktoré sú výsledkom spoločnej práce s P. Ďurišom, Ri. Královičom a R. Korbašom. Zameriame sa na vzťah determinizmu a nedeterminizmu - kým nedeterministické automaty vedia s exponenciálnou radou akceptovať ľubovoľný jazyk (a sú jazyky, ktoré exponenciálnu radu potrebujú), deterministické automaty nedokážu akceptovať niektoré jednoduché jazyky bez ohľadu na veľkosť rady. Zaujímavá otázka je, akú veľkú radu dokážu deterministické automaty využiť: ukážeme, že ak sa jazyk nedá akceptovať s exponenciálnou radou, nedá sa akceptovať vôbec. Máme hypotézu, že deterministický automat nedokáže využiť viac ako polynomiálnu radu. Ukážeme tiež hierarchie v závislosti od veľkosti rady pre nedeterministické automaty.

9. 3. 2018, 11:00

Broňa Brejová

(KI FMFI UK)

   Izometrická rekonciliácia génových stromov

Na seminári sa budeme venovať problému rekonciliácie génových a druhových stromov z oblasti bioinformatiky. V tradičnej verzii problému sú obidva stromy zadané iba svojou topológiou a cieľom je nájsť zobrazenie medzi ich vrcholmi minimalizujúce určitú mieru súvisiacu s počtom evolučných zmien. My však študujeme verziu problému, v ktorej obidva stromy majú známe aj dĺžky hrán a zobrazenie je tým jednoznačne dané. Prvé výsledky sme už prezentovali na seminári v roku 2016, odvtedy však máme nové výsledky aj nové otvorené problémy.

Spoluatori Askar Gafurov, Radoslav Chládek, Dana Pardubská, Michal Sabo, Tomáš Vinař

16. 3. 2018, 11:00

Peter Kostolányi

(KI FMFI UK)

   Algebraické systémy nad sumačnými polokruhmi

Algebraické systémy nad polokruhmi sú známym zovšeobecnením (aj) bezkontextových gramatík, pri ktorom sa od generovania bezkontextových jazykov (čiže algebraických prvkov v polokruhu formálnych jazykov) prechádza k realizácii algebraických prvkov v nejakom všeobecnejšom polokruhu. Nie je ale možné zmysluplne definovať prvok realizovaný ľubovoľným algebraickým systémom nad ľubovoľným polokruhom - a to ani v prípade, že sa obmedzíme na najčastejšie skúmaný špeciálny prípad polokruhov nekomutatívnych formálnych mocninových radov. Typická prezentácia teórie algebraických systémov tak zvyčajne začína voľbou: buď sa pozornosť venuje len nejakej špeciálnej triede polokruhov, ako sú napríklad spojité polokruhy alebo úplné polokruhy, alebo sa nad všeobecným polokruhom mocninových radov pracuje len so systémami spĺňajúcimi určité podmienky. To je obzvlášť nepríjemné z dôvodu, že výsledné teórie vykazujú mnohé spoločné znaky.

Na prednáške predstavíme zjednocujúci prístup k definovaniu algebraických prvkov polokruhu, ktorý eliminuje nutnosť tejto voľby tým, že zahŕňa obidva zvyčajné prístupy (to možno z časti prirovnať efektu Ésikovej a Kuichovej zjednocujúcej teórie racionálnych prvkov polokruhu, ktorá ale využíva odlišné prostriedky). Pôjde o metódu založenú na pojme sumačného polokruhu (ide tu o premenovanie Sigma-polokruhov Hebischa a Weinerta) a na priraďovaní určitých jednoznačných bezkontextových jazykov premenným každého algebraického systému. Na tejto všeobecnej úrovni potom dokážeme dva klasické výsledky pre algebraické systémy: ich ekvivalenciu so zásobníkovými automatmi a Chomského- Schützenbergerovu vetu o reprezentácii. Prínosom prezentovaného prístupu tiež bude možnosť dokazovať určité tvrdenia pre algebraické systémy nad polokruhmi ako jednoduché dôsledky známych tvrdení pre bezkontextové jazyky.

13. 4. 2018, 11:00

Dušan Guller

(KAI FMFI UK)

   On Multi-step Fuzzy Inference in Goedel Logic

Recent years witness a prospective application potential of the fuzzy logic and inference approach to emerging technologies in the area of artificial, computational intelligence, and soft computing. Fuzzy rules and one-step fuzzy inference is widely exploited in fuzzy controllers since the seventies. From a viewpoint of artificial intelligence, such a kind of inference has a reactive behavior. In contrast to control purposes, one-step fuzzy inference is not sufficient for so-called fuzzy reasoning, where some kind of abstract inference is needed to reach a reasonable conclusion, which stipulates multiple inference steps.

In our talk, we will discuss the logical and computational foundations of multi-step fuzzy inference using the Mamdani-Assilian type of fuzzy rules by implementing such inference in Goedel logic with truth constants. We apply the results achieved in the development of a hyperresolution calculus for this logic. We pose three fundamental problems: reachability, stability, the existence of a k-cycle in multi-step fuzzy inference and reduce them to certain deduction and unsatisfiability problems. The corresponding unsatisfiability problems may be solved using hyperresolution.

20. 4. 2018, 11:00

Richard Ostertág

(KI FMFI UK)

   Bezpečnosť elektronických prístupových systémov

Klasické kľúčové prístupové systémy sú dnes už čoraz častejšie nahrádzané elektronickými. V hoteloch namiesto kľúčov od izby používame karty. Garážové brány otvárame diaľkovým ovládaním. Do panelákových vchodov si dvere otvárame elektronickým kľúčom – príveskom. Autá otvárame bezdrôtovo na diaľku. Všetci vieme, že mnohé zámky dokážu šikovní zámočníci otvoriť aj bez kľúča. Je to tak aj s elektronickými zámkami? V tejto prednáške sa pozrieme na bezpečnosť vybraných elektronických ekvivalentov fyzických kľúčov a ukážeme si aj princípy niektorých útokov na elektronické kľúče.

27. 4. 2018, 11:00

Rasťo Královič

(KI FMFI UK)

   Tight Hierarchy of Data-Independent Multi-Head Automata

We study the expressive power of 1-way data-independent finite automata with multiple heads. The data-independence means that the trajectory of each head during a computation on an input word w depends only on the length of w. An important question in the understanding of various versions of multi-head automata, is whether additional heads increase the expressive power. For the data-dependent 1-way automata, the famous result by Yao and Rivest established, as early as in 1978, a tight hierarchy that L(1DFA(k)) is a strict subset of L(1DFA(k + 1)). In 1980, Monien proved similar tight hierarchy for 2-way automata, both deterministic and non-deterministic. As noted by Holzer in 2002, Monien’s results yield a tight hierarchy for 2-way data-independent automata. However, somewhat surprisingly, no such hierarchy has been known for the 1-way data-independent automata. We show not only the tight hierarchy for 1-way data-independent automata, but even stronger result as well, that for each k>0, there are languages that can be recognized by a data-independent automaton with k + 1 heads, but cannot be recognized with k heads even with non-deterministic data-dependent automaton. On the other hand, we show that if the non-deterministic automaton is allowed to be two-way, 8 heads are sufficient to simulate all data-independent 1-way automata. Finally, we remark that the restriction of data-independence cannot be compensated by adding more heads, as there are languages that can be recognized by a 1-way deterministic automaton with 2 heads, but cannot be recognize by any data-independent automaton, regardless of the number of heads.

11. 5. 2018, 11:00

Róbert Lukoťka

(KI FMFI UK)

   Deciding 3-edge-colourability of graphs.

We present three ideas that can be used to improve running times of algorithms deciding 3-edge-colorability of graphs. We show two ways how to efficiently transform a 3-edge-coloring into an improper 2-vertex coloring using balanced valuations [F. Jaeger: Balanced Valuations and Flows in Multigraphs, Proceedings of the American Mathematical Society 55 (1976)] or embeddings into orientable surfaces. Finally, we sketch how Hilbert's Nullstellensatz can be used to provide a certificate that a graph is not 3-edge-colourable [J. A. De Loera, J. Lee, P. N. Malkin, S. Margulies: Computing infeasibility certificates for combinatorial problems through Hilbert's Nullstellensatz, Journal of Symbolic Computation 46 (2011), 1260-1283].

31. 5. 2018, 11:00

Warren A. Hunt, Jr.

(UT Austin)

   Industrial Hardware and Software Verification with ACL2

The ACL2 theorem-proving system has seen sustained industrial use since the mid 1990s. Companies that have and are using ACL2 include AMD, ARM, Centaur Technology, General Electric, IBM, Intel, Kestrel Institute, Motorola/Freescale, Oracle, and Rockwell Collins. ACL2 has been accepted for industrial application because it is an integrated programming/proof environment supporting a subset of the ANSI standard Common Lisp programming language. Software and hardware systems have been modeled and analyzed with the ACL2 theorem-proving system.

The ACL2 programming language can be used to develop efficient and robust programs. The ACL2 analysis machinery provides many features permitting domain-specific, human-supplied guidance at various levels of abstraction. ACL2 specifications often serve as efficient execution engines for the modeled artifacts while permitting formal analysis and proof of properties. ACL2 provides support for the development and verification of other formal analysis tools. ACL2 did not find its way into industrial use merely because of its technical features. The ACL2 user/development community has a shared vision of making formal specification and mechanized verification routine -- we have been committed to this vision for the quarter century since the Computational Logic, Inc., Verified Stack.

Spoluautori:

Matt Kaufmann, J Strother Moore (Dept. of Computer Science, UT Austin)

Anna Slobodova (Centaur Technology, Inc. Austin, Texas)