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