Ettekanded

 

EnnTõugu: Loogika riistvara/tarkvara koodisaini spetsifitseerimiseks (A Specification Logic for HW/SW Codesign)

Kokkuvõte: A common formal basis for representing the semantics of computations both on the level close to hardware primitives, and on the level of software components is presented. This logic is expressive enough for describing, first, the structure of hierarchical configurations and, second, dataflow both on signal and object level. It is sufficiently efficient for synthesis of large configurations and algorithms from their high-level specifications. A specification language based on this logic is outlined and an example is presented
 

Merik Meriste, Leo Mõtus, Tõnis Kelder, Jüri Helekivi, Vadim Kimlaychuk: Ajatundlike agentide testimissüsteem – mõned asjassepuutuvad probleemid (A test-bed for time-sensitive agents - some involved problems)

Kokkuvõte: This presentation discusses design issues of a test-bed for multi-agent systems, especially aspects that are related to enabling formal analysis of behaviour generated by agents and groups of interacting agents. The test-bed is to be used, among other conventional things, for specifying and formal analysis of time aspects, related to Quality of Service - e.g. requirements and constraints for correct functioning, activation periods, correct frequency and/or instants of interactions, correct age of the used data and events, and other properties. All those timing requirements and constraints are essential for proper operation of a multi-agent system in a time-critical application, for analysis of overall design and implementation related properties, as well as for guaranteeing certain properties of emergent behavior during operation of a multi-agent system. The analysis of properties that stem from adaptation, learning, and decision-making of an agent, will not be discussed (although we believe that those processes can be studied by using similar model of computation).
 

Vahur Kotkas: Hajusprogrammide süntees.

Kokkuvõte: Oma ettekandes tutvustan ühte võimalikku programmide sünteesi meetodit. Selleks kasutame Java programme, mille lähtekood on laiendatud deklaratiivsete spetsifikatsioonidega. Programmid võivad vajadusel välja kutsuda süntesaatori, mis nende spetsifikatsioonide ja ülesandepüstituse alusel koostab uue programmi ja käivitab selle. Käivituse tulemused edastatakse sünteesi välja kutsunud programmile. Antud raamistikus on mitmeid võimalusi kuidas programmide süntesaatorit ja sünteesitavaid programme oleks võimalik käivitada hajusal arhitektuuril.
 

Marko Kääramees: Raamvärk lõpmatu olekuruumiga süsteemide verifitseerimiseks kontranäidete abiga täpsustatavate abstraktsioonide kaudu

Kokkuvõte: Lõpmatu olekuruumiga süsteemide verifitseerimisülesanne ei ole üldjuhul
lahenduv. Alati leidub verifitseeritavale omadusele abstraktsioon,
millega saab probleemi lõplikuks taandada, aga selle abstraktsiooni
leidmiseks pole konstruktiivset algoritmi. Vaatame üht üldist algoritmi,
millega on võimalik abstraktsiooni järkjärguliselt täpsustada kasutades
kontranäiteid, mis rikuvad verifitseeritavat omadust abstraktses
süsteemis, aga mitte konkreetses.
 

Tanel Tammet: Combining an inference engine with web databases: a rule server

Kokkuvõte: Complex semantic web applications require easy-to-use tools for data and rule storage along with query mechanisms. We describe a prototype server software RLS which is used similarly to the ordinary usage of SQL servers in application programming. The server combines first-order theorem provers with several query and rule language layers for application development in the Semantic Web context.
 


Mihhail Svintsov: Evolutsioonilised algoritmid neuronvõrkude õpetamisel ja genereerimisel

Kokkuvõte: Vaadeldakse neuronvõrkude loomise ja õpetamise viise evolutsiooniliste algoritmide abil. Põhieesmärgiks on nende kahe analüütilise tehnoloogia ühendamise võimaluse uurimine. Kirjeldatakse evolutsioonilistel algoritmidel baseeruvaid meetodeid, mis arvestavad neuronvõrgu topoloogia eripära. Välja on töötatud algoritmid, mis võimaldavad nii õpetada neuronvõrke kui ka luua optimaalse topoloogiaga neuronvõrke.


 
 

Jaan Penjam, Jelena Sanko: Deduktiivne ja induktiivne programmide süntees

Kokkuvõte: The paper discusses simple functional constraint networks and value propagation method for program construction. Structural synthesis of programs is described  as an example of deductive approach to program construction. An inductive method for program synthesis    utilizing stochastic optimization algorithms is introduced to complement value propagation techniques.
 

Jaanus Pöial: Programmianalüüs magasinorienteeritud keelte jaoks

Kokkuvõte: Ettekandes tutvustatakse programmianalüüsi meetodite kasutamist magasinorienteeritud keeltes kirjutatud tarkvara (kiipkaardid, väheste ressurssidega sardrakendused, ...) analüüsimiseks eesmärgiga leida programmidest magasini kasutamise vigu. Efektiivne on just "peab"-analüüsi rakendamine "võib"-analüüsi asemel, sest analüüsi aluseks olev matemaatiline struktuur ei ole võre vaid poolvõre (elementide hulgale saab leida suurimat alumist raja, aga ei saa leida vähimat ülemist raja). On defineeritud reeglid hargnemiste ja tsüklite käsitlemiseks (varem sai uuritud ainult lineaarset programmikoodi). Tulemusi illustreerib Javas kirjutatud raamistik "peab"-analüüside arvutamiseks.
 

Varmo Vene, Tarmo Uustalu:  Termineeruv rekursioon ja rekursiivsed koalgebrad

Kokkuvõte: Nagu hästi teada, on rekursiivselt defineeritud funktsiooni termineeruvuse staatiliselt kindlaks tegemine on algoritmiliselt lahendamatu probleem. Seetõttu on nn. tugevas funktsionaalprogrammeerimises aktiivset uurimist leidnud keeled, kus üldrekursiivsed definitsioonid pole lubatud, vaid tuleb kasutada spetsiifilisi rekursioonioperaatoreid, mis tagavad programmide termineeruvuse konstruktsiooni kohaselt. Ettekandes vaatleme termineeruvaid rekursiooniaperaatorid, mis on indutseeritud teatavate omadustega koalgebrate poolt. See võimaldab käsitleda paljusid varem uuritud spetsiifilisi konstruktsioone ühtses formalismis ning loob
võimaluse nende üldistamiseks. Muuhulgas demonstreerime komonaadilise rekursiooni üldistust antud raamistikus.

 

 


 

Jaan Penjam
Merik Meriste
Varmo Vene
Viimane uuendus 3.9.2003