Otázky

Podrobnější znění otázek lze nalézt na webu Petra Tůmy. Píše se tam, že uvedené znění "by mělo vejít v platnost ve školním roce 2005/2006". To se opravdu stalo, tj. otázky přesně odpovídají.

Níže je seznam užitečných materiálů k jednotlivým otázkám. Některé odkazy vedou na materiály na webu předětu Objektově orientované systémy, které jsou zaheslované. O heslo si lze napsat vyučujícím.

Pro přehlednost jsou názvy otázek v nadpisech uvedeny stručně, tj. bez podrobností v závorkách.

Třídy a objekty

Prototypy a klony

Výpisky

Programování založené na prototypech je styl OOP, kde nejsou třídy a chování objektů je definováno pomocí klonování a upravování existujících objektů. Nový objekt je označován jako klon, předloha jako prototyp. Motivací je mimo jiné to, že je problém navrhnout optimální (i do budoucna) hierarchii tříd v klasickém class-based přístupu.

Pojmy

  • Method slot – v Selfu jsou objekty kolekcemi slotů. Slot může obsahovat buď proměnnou (field) nebo metodu. Pokud je to proměnná, tak "se tváří" jako přístupová metoda, která může proměnnou číst (myPerson name) nebo zapisovat (myPerson name: 'Janek').

  • Parent slot – je slot který ukazuje na rodičovský objekt, což umožňuje delegovat neznámé zprávy (neodpovídající žádnému z lokálních slotů) na takto označený rodičovský objekt (např. to může simulovat dědičnost či interfacing).

  • Trait – parametrizovaná sada metod, která slouží jako základní stavební blok pro definování chování tříd (http://www.iam.unibe.ch/%7Escg/Research/Traits/). V Selfu jsou to objekty, které se hodí strkat do parent slotů.

  • Mixin – souvisí s postupem, kdy je objekt "smíchán" z více jiných objektů (či tříd) tak, že je podtypem každého z nich (např. pomocí vícenásobné dědičnosti v klasickém class-based OOP, nebo pomocí parent slots v Selfu). Zdroje se různí v tom, zda mixin je výsledek, nebo "ingredience".

Dědičnost a subtyping

Subsumptions => Subtyping

  • definuju vztah subsumption (<:) mezi typama, pro kterej plati, ze kdyz T1 <: T2, tak na instance T2 se muzu koukat jako na instance T1

  • pokud pro tenhle vztah plati: instance tridy C1 jsou ve vztahu <: s instancema tridy C2, prave kdyz C1 je podtrida C2

  • tak to implikuje subtyping

Objekty v distribuovaném prostředí

Výpisky

CORBA (Common Object Request Broker Architecture)

  • IDL připomíná C++, typy:

    • interger, FP, character (char + wchar), boolean, special types (octet, any)

    • structures, unions, enums, arrays, sequences, strings, fixed point types, exceptions, interfaces, value types (předán hodnotou a přistupován lokálně)

  • mapování do jazyků

    • v C++ se řeší problém s velikostí pomocí typedefů, správu paměti řetězců pomocí tříd s alokátory,...

    • v Javě se řeší problém s "direction" (typeinfo, serializace, ?) pomocí Holder classes, velikost pomocí data conversion exception

    • interfaces: type casting zavedením narrow v obou jazycích, v C++ memory management pomocí var classes a reference countingu

  • [portable] object adapter – configuration, policies,...

  • síťový protokol – GIOP definuje Common Data Representation (CDR), Message Formats a Transport Assumptions; IIOP je GIOP over TCP/IP

RMI (Remote Method Invocation)

  • specifikace rozhraní v Javě, použití standardní serializace

  • vzdálený objekt musí implementovat interface Remote, metody hážou RemoteException

  • implementační objekt dědí nepřímo od RemoteObject (UnicastRemoteObject – export/unexport, nebo Activatable – perzistentní objekty)

  • life cycle – lokálně garbage collection, vzdáleně reference counting + keepalive (leasing)

  • existuje RMI-IIOP pro interoperabilitu s CORBA

  • Základní prvky: Client, instance ServerObject implements RemoteInterface, běžící RMI registry (naming)

Replikace a mobilita v distribuovaném prostředí

Výpisky

Replikace je klíčová technika distribuovaných systémů. Mohou být replikována data, nebo celé výpočty (data i program). Při replikaci pouhých dat jsou výsledné procesy pasivní (vyřizují jen read requesty) a dodatečně aplikují updaty. Při replikaci výpočtů je obvykle motivací dosažení fault-tolerance.

Problémem je např. nutnost vynutit pořadí přicházejících zpráv, pokud chceme, aby si všechny replicas udržovaly identický stav (viz např. wen:Atomic%20broadcast).

Mobilita se týká mobilních agentů. Mobilní agent je autonomní program, který může migrovat mezi hostiteli v heterogení síti (včetně zachování aktuálního stavu [výpočtů]), kdykoli a kamkoli "se mu zachce". To se hodí pro distribuované "výpočty", výhodou je robustnost, kterou přináší autonomie (~absence centrálního řízení výpočtu). Může to také redukovat latenci a bandwith například tím, že celý program dočasně "přeskočí" ze serveru na klienta, čímž eliminuje častou komunikaci mezi klientem a serverem. Problémy konceptu jsou mimo jiné: agent fault tolerance, agent security, a inter-agent communication and synchronization.

Konzistence replikace:

  • atomic broadcast

  • FSM

Modely konzistence bez synchronizace

  • striktní - poslední write je okamžitě vidět v celém systému (v reálu náročné)

  • sekvenční

    • výsledek jakékoli operace proběhne tak, jako kdyby čtení a zápisy všech procesů proběhly v nějakém pořadí (tj. jakékoliv uspořádání striktně konzistentní)

    • operace každého procesu jsou v systému vidět v tom pořadí, ve kterém je proces vykonal

  • lineární - silnější než sekvenční - operace s menším časovým razítkem jsou vidět dřív operace s vyšším TS

  • kauzální - potenciálně navazující zápisy musí být vidět ve správném pořadí v celém systému, konkurentní mohou být vidět na různých místech různě

  • FIFO - zápisy jednoho procesu jsou v celém systému vidět ve stejném pořadí, od různých procesů na různých místech různě

Modely konzistence se synchronizací

  • weak - data konzistentní pouze po synchronizaci

  • release - data konzistentní při opuštění kritické sekce

  • entry - data konzistentní při vstupu do kritické sekce

Metody replikace vypoctu:

  • State Machine Replication

    • FSM reprezentujici praci s datama se umisti na kazdy server

    • pri startu repliky zacnou ve stejnym stavu; kazda operace zmeni vsem stav a generuje vystup

    • kazdy z automatu obdrzi inputy ve stejnem poradi a updatne FSM

    • stavy a vystupy se porovnaji (kontrola chyb, konzistence) a jeden vystup se odesle klientovi

    • je to teda aktivni replikace (IMO)

    • pouziva napr. Google Chubby

      • primary-backup

      • zamky a male soubory

      • 5 replik, sdileji kod

      • replikuje se databaze

  • Virtual Synchrony

    • procesy se sdruzujou do skupin

    • prichozy zpravy se dorucej ve stejnym poradi vsem clenum skupiny

    • zmena clenstvi ve skupine nebo crash procesu se taky posila jako zprava

    • virtualni je to proto, ze se obcas zpravy prehazou pro zvyseni vykonu (ale jen kdyz by to procesu bylo jedno)

    • taky asi aktivni replikace; multi-primary

    • pouziva napr. CORBA

Metody replikace dat na discich:

  • synchronous - ceka na potvrzeni akce od vsech zucastnenych -> snizeni vykonu (v zavislosti na fyzicke vzdalenosti serveru)

  • asynchronous - neceka, takze je rychlejsi, ale je tam prodleva, ve ktery je risk, ze server crashne a replika nebude hotova

  • semi-synchronous - ceka se jen az vzdaleny server potvrdi prijeti dat, ale neceka se na jejich zapis

Migrace procesu:

  • vyvazovani zateze; neovlivni ostatni procesy; transparentni

    1. zastaveni procesu ze zdroje Z (zmrazeni, specialni stav)

    1. priprava cile C

    1. prenos stavu procesu a adresoveho prostoru na C

    1. docasne presmerovani zprav na C (nez vsichni vedi o presunu)

    1. vycisteni procesu na Z a spusteni na C

  • predp. OS ma prostredky vic transparentni: zamky (Chubby), soubory na distr. FS, abstrakce nad socketama

  • problemy:

    • prostredky (viz. vyse)

    • sdilena pamet (emulace pres sit)

    • presmerovani I/O (distr. FS)

    • IPC (nutno presmerovat komunikaci mezi "lokalnima" procesama, ktery uz nejsou lokalni)

Pojmy:

  • Replica – jedna z instancí [replikovaného] výpočtu (agenta)

  • Active replication – stejný požadavek zpracovávají všechny replicas

  • Passive replication – požadavek zpracovává jen jedna replica a výsledek je přenesen do ostatních

  • Primary-backup - jeden proces dela vsechno a jen posila zmeny druhemu; drahe, protoze ten druhej nic kloudnyho nedela

  • Multi-primary - vsechny procesy neco delaj; distribuovane se nejak synchronizujou; problem pro databaze

Vyhledávání prostředků

Výpisky

CORBA umí uložit referenci do stringu (a uložit do souboru) a z něj vytvořit proxy (object_to_string() a string_to_object()), vhodné pokud klient a server sdílí file systém.

CORBA Naming Service

  • mapování (human-readable) názvů na IORy

  • uloženo hierarchicky, adresáře (= naming contexts) jsou taky CORBA objekty (může být uloženo distribuovaně)

  • aplikace můžou importovat a exportovat objekty pomocí naming service (musí znát příslušnou cestu, ta obvykle sídlí někde v konfiguráku), např.:

  obj = importObjRef(orb, "name_service#path/in/Naming/Service")  exportObjRef(orb, obj2, "file#/path/to/file.ior")

  • starej interface (importObjRef vyzaduje utility knihovnu):

  NamingContextExt namingServiceExt = NamingContextExtHelper.narrow(orb.resolve_initial_references("NameService"));  obj = namingServiceExt.resolve_str("path/in/Naming/Service");  namingServiceExt.bind(namingServiceExt.to_name("path/in/Naming/Service"), obj);  // nebo  namingServiceExt.bind(new NameComponent[]{new NameComponent("path",""), new NameComponent("in",""), new NameComponent("Naming",""), new NameComponent("Service","")}, obj);

  • naming services jdou propojovat (tzv. federation), pak se k nim pristupuje jako k celku

CORBA Trading Service

  • podobný jako naming service, připomíná zlaté stránky telefonního seznamu

  • nabízí služby spolu s referencí (IOR) a popisem, organizované do kategorií (service offer types)

  • kategorie jsou definovány pomocí rozhraní ServiceTypeRepository

  • aplikace exportují reference pomocí rozhraní Register

  • rozhraní Lookup definuje operaci query, která umožňuje vyhledat službu podle nějaké podmínky

  • podobně jako naming service je možné trading services propojovat

  • pro obě služby existují utilitky (cmd-line i GUI) pro administraci, což redukuje kódování

  • priklad v Jave:

  Lookup lookup = LookupHelper.narrow(orb.resolve_initial_references("TradingService"));  // register type  PropStruct[] props = new PropStruct[]{new PropStruct("resolution", CORBA.INTEGER, PropertyMode.PROP_NORMAL)};  String[] superTypes = new String[]{new String("OfficeDevice")};  lookup.serviceTypeRepository.add_type("Printer", "IDL:acme.com/Equipment/Printer:1.0", props, superTypes);  // register object  Property[] properties = new Property[]{new Property("resolution", 300};  lookup.register.export(obj, "Printer", properties);  // search for it  Offer[] offers= lookup.query(    "Printer", // type name    "resolution >= 300", // constraint    "resolution", // preferred properties (influences sorting of the results)    ...);  obj = offers[0].reference;

JNDI (Java Naming and Directory Interface)

API adresářové služby, nabízí:

  • mechanismus pro navázání (bind) objektu na jméno

  • directory lookup iface pro obecné dotazy

  • rozhraní pro události, které informují klienta o změně adresářových položek

  • Service Provider Interface (SPI) pro napojení jiných adresářových služeb (LDAP, CORBA naming service,...)

  • příklad:

Object reference = myCurrentContext.lookup("com.mydomain.MyBean");MyBean myBean = (MyBean) PortableRemoteObject.narrow(reference, MyBean.class); // this step is needed for EJB beans

UDDI (Universal Description Discovery and Integration)

  • markup language zalozeny na XML

  • register webovych sluzeb

  • rozdelen na:

    • white pages - prime kontakty na jednotlive sluzby / businesses

    • yellow pages - sluzby jsou razene do kategorii

    • green pages - technicke detaily o pristupu k dane sluzbe; jak se pripojit, atd.

  • komunikace jde pres SOAP zpravy

Garbage collection

Výpisky

Garbage collection je způsob automatické správy paměti. Garbage Collector (GC) uvolňuje paměť, která již nebude použita.

  • vyhody

    • zamezeni dangling pointer bugu

    • zamezeni double free bugu (2x uvolnena pamet)

    • zamezeni leakum (nekterym)

  • nevyhody

    • overhead

    • unpredictable

    • stale zustaji logical leaks

    • poor locality -> thrashing

  • syntactic vs. semantic garbage (~halting problem), dá se pracovat jen se syntactic garbage

  • reachability tracing

    • mark and sweep – naive vs. tri-color (white-gray-black)

    • moving vs. non-moving – moving přesouvá platné objekty a zahazuje celou oblast, to zjednodušuje uvolňování, snižuje fragmentaci, atd, ale musí relokovat pointry, pokud jsou v objektech obsaženy (třeba .NET). Také se tomu říká mark and compact.

    • copying GC – je moving GC, který uklízí tak, že postupně kopíruje dosažitelné objetky do nové oblasti (místo obarvování). Může je i v původní paměti dočasně nechat, nebo tam nechat pointer na nová data (tzv. "broken heart") -> inkrementální GC.

    • concurrent GC – běží zároveň s hlavním programem (na druhém procesoru, nebo aspoň v druhém vlákně)

        1. pauzne se mutator (kratce); oznaci se sede objekty primo dostupne z rootu

        1. mutator bezi; oznacujou se sedive objekty; zmeny delane mutatorem se oznacuji

        1. pauzne se mutator (kratce); zpracujou se objekty oznaceny jako zmeneny

        1. mutator bezi; sweepuje se, ale bez scukavani

    • na půl cesty mezi stop-the-world a concurrent přístupy je incremental GC – ten přerušuje svou práci a dovoluje běh hlavního programu (mutatoru). Ale nesmi ho nechat, aby dostal nekonzistentni data, takže na chvíli povoluje i duplicity.

    • mutátor je oznaceni pro cast kodu, ktera pracuje s referencema na objekty (typicky je to user aplikace). V inkrementalnim GC kdyz bezi GC, tak se mutator pauzne, GC doresi nakou svoji fazi a mutator se opet pusti. V concurrent GC muzou oba bezet najednou (vetsinu casu)

    • finalizer je neco jako destruktor, ale spusteno az pri mazani objektu, coz muze bejt za dlouho; resi uvolnovani nepametovych resourcu (soubory)

  • reference counting

    • každý objekt má počítadlo referencí, když klesne na nulu, je oznacen pro uvolneni; je problém s cykly

    • vyhody: lepsi pro real-time; snazsi implementace; efektivni pro nepametove zdroje (soubory); nema problem se skoro zaplnenou pameti

    • nevyhody: vyzaduje caste updaty pocitadel (pri kazdem create, destroy, zmene reference -> problem s cache a CPU pipeline); problem s cyklickou referenci

    • deferred increments odlozi zmenu counteru u lokalnich promennych na pozdeji - casto se ukaze, ze by byla zbytecna, protoze u lokalnich promennych vznikne a zanikne reference kratce po sobe

    • reseni cyklu: zakazat v jazyku; ignorovat; pouzit na cykly tracing collector

    • v distribuovaném prostředí je potřeba používat reference counting, nebo nějakou keepalive strategii, tj. reference musí občas objektu sdělit, že má být ještě naživu. Reference counting na distribuovaném prostředí je weighted. Při kopírování reference se jeji váha dělí na půl mezi originál a kopii a není potřeba zasílat inkrementovat pocitadlo na objektu. Pocitadlo pocita celkovou vahu, ne pocet referenci. Pocitadlo se zmeni jen při smazání reference (ale někdy je zase nutné zvýšit celkovou váhu).

Architektura komponentových systémů

Výpisky

Softwarová komponenta:

  • dobre definovane chovani (dle modelu)

  • dobre definovane interfacy (dle modelu)

  • nezavisly deployment

Deli se:

  • funkcionalitou – provides/requires

  • způsobem integrace – nesting (hierarchie)

  • způsobem nasazení (deployment/packaging) – adresový prostor, kontejner, .jar soubor

  • run-time chováním (run-time monitoring,...)

  • způsobem dynamického nahrazování (rekonfigurace architektury, verzování)

Pravidla pro tyto vlastnosti jsou určena komponentovým modelem.

Jde o vyšší úroveň abstrakce, než jsou objekty z OOP. Hlavním cílem je snadná opakovaná použitelnost funkcionality (a v důsledku kódu, který ji poskytuje).

component sharing

  • kdyz vice komponent chce sdilet svoji podkomponentu, napr. DB

  • sdilena komponenta je podkomponentou vice komponent, ale existuje jen jedna jeji instance

  • nak to de ve Fractalu

JavaBeans

  • motivace: jednoduchý design GUI

  • BeanBox (environment, container, single address space), naming conventions for classes, publisher-subsciber

  • pouze provided interface: gettery/settery, metody, events (pres listener)

EJB (Enterprise JavaBeans)

  • motivace: jednoduché object-like komponenty pro snadný přístup do relačních databází

  • flat model

  • Bean

    • Entity (persistence) – v EJB 3.0 nahrazeno wen:Java%20Persistence%20API (persistence, obj.-rel. mapping)

    • Session (stateful/stateless) – zajišťují nějakou funkcionalitu pro uživatele

  • kontejner poskytuje: Security, Life-cycle, Persistence, Transactions, Remote Access (via RMI)

  • EJB 3.0 jsou více lightweight, používají se wen:%20Java%20annotations (Java 5.0 feature) místo "deployment descriptors"

    • inspirace v "konkurečních" projektech Hibernate (persistence a obj.-rel. mapping) a Spring Framework (business logic)

  • EJB home - neco jako factory pro komponenty

CCM

  • motivace: real-time systemy, platform independent

  • flat model

  • implicit connectors (CORBA-based communication)

  • provides (facet) / requires (receptacle)

  • publisher (event source) / subscriber (event sink)

  • home - neco jako factory pro komponenty

  • IDL misto ADL

    • navic pridano component { provides uses emits consumes }

SOFA 2

  • hierarchical model

  • connectory mezi interfacama - delegace, zpravy, listenery

  • deployment: SOFA nodes, deployment dock (container), repository (of components; automaticky se nahravaj do docku)

  • SOFA ADL

    interface IMyComp { void m1(); void m2(); ... protocol: m2; (m1); m2};frame MyComp { requires: IOtherComp req; provides: IMyComp prov; protocol: !req.init; ?prov.m2; (?prov.m1); ?prov.m2; !req.finish};frame MyInnerComp { requires: IOtherComp innerReq; provides: IMyComp innerProv; protocol:};architecture MyComp implements MyComp { inst MyInnerComp inner1, inner2; subsume inner1:innerReq to req bind inner1:innerProv to inner2:innerReq delegate inner2:innerProv to prov};

  • primitive component - obsahuje implementaci, ostatni komponenty jsou slozeny z jinejch komponent

    public class MyInnerComp { @Required(name="innerReq") public IOtherComp required; @Provided(name="innerProv") public IMyComp provided; @Start public void letsdoit() { /* spawn a thread and do something */ }};

Darwin

  • ADL, hierarchicky, dynamicke architektury, vyzkumny

    component Inner1 { require req; provide prov; }component Inner2 { require req; provide prov; }component MyComp { require req; provide prov; inst A:Inner1; B:Inner2; bind req -- A.req; A.prov -- B.req; B.prov -- prov;};

(D)COM

  • motivace: interoperabilita jazyků, dynamické zjišťování rozhraní

  • C++ polymorfizmus

  • interface IUnknown (metody QueryInterface, AddRef, Release)

  • DCOM – distribuovaný

    • pres RPC

WRIGHT

  • ADL (architecture description language)

  • formálně popisuje architekturu systému (komponenty, konektory,...)

  • popisuje chování pomocí CSP-like syntaxe (wen:Communicating%20Sequential%20Processes)

  • umožňuje definovat a staticky kontrolovat nějaké vlastnosti systému

Specifikace chování systémů

Kripke Structure

  • NKA

  • stavy odpovidaj mistum v kodu

  • ke kazdymu stavu labeling function priradi podmnozinu propositions (hodnot promennejch)

  • vrcholy stavovyho grafu jsou pak ruzny pro ruzny kombinace stav/propositions (do stejny casti programu se muzu dostat s jinou konfiguraci promennejch)

  • nema prijimaci ani konecne stavy, vypocet nikdy nekonci (zaridim treba cyklem na konci)

Labelled Transition System (LTS)

  • ke Kripkeho strukture navic prirazuje labely k prechodum

  • labely odpovidaji akcim, napr. prirazeni hodnoty

  • dohromady tvori State Transition System

  • trace: posloupnost kroku z nakyho stavu; ala derivace v automatech

  • zkoumani ekvivalence ruznych LTS, napr. pomoci porovnani traces (trace-ekvivalence)

Communicating Sequential Processes (CSP)

  • process algebra

  • primitives:

    • procesy (napr. STOP); seriove i paralelni (naproti nazvu)

    • events: komunikace mezi procesy

Verifikace

  • dokazuju, ze SW odpovida pozadavkum: testovani nebo formalne

Problemy testovani a verifikace

  • u model checkingu

    • semanticka mezera mezi kodem a modelem

    • state explosion

    • jak zformalizovat pozadavky na system?

    • neni vhodnej pro flat modely, ale spis pro hierarchicky komponentovy modely

  • u dokazovani vlastnosti

    • imperativni programy a side-effecty

Slozitost dokazovani

  • u dokazovani vlastnosti obecne nerozhodnutelnej problem (viz. problem ekvivalence dvou programu: modelu a skutecnyho)

  • ale u model checkingu je uz rozhodnutelny checkovani nekonecne stavovyho systemu konecnym modelem

  • staticka analyza (napr. pouziti promenny bez inicializace, nekonecnej cyklus, atd.) je nerozhodnutelny

Model checking

Uloha Model Checkingu

  • pro predchazeni problemum, obvijouzli

  • Finite-State Model + Temporal Logic Formula -> Model Checker -> OK | Error Trace

  • model construction: potreba namapovat programovaci jazyky na konstrukci automatu

  • property specification: chceme psat omezeni na urovni kodu, ale v logice pracujem s modelem (automatem)

  • output interpretation: error trace muze bejt hodne dlouhy, navic je vyjadreny ve stavech automatu

  • jak se to dela:

      1. prepisu program do pseudokodu

      1. udela se z toho Kripkeho struktura

      1. z ni se udela Buchiho automat BA1 (KA prijimajici nekonecny slova). Beh na nekonecnym slovu prijme, pokud nekonecnekrat slapnu na prijimaci stav

      1. definuju LTL formuli pro 2)

      1. z negace 4) udelam zase Buchiho automat BA2

      1. udelam prunik BA1 a BA2 -> BA3

      1. pokud ma BA3 prazdnej jazyk, tak negace neplati a formule plati

State Explosion

  • limitovat model checking jen na oddelenou jednotku programu, pro snizeni poctu stavu

  • problem v OOP, kde mizi hranice mezi castmi programu (reference, callbacky)

  • jiny reseni je graf FSM reprezentovat implicitne vyjadrenim ve formulich

  • dalsi reseni je zkoumat vypocet FSM do maximalne k kroku a k postupne zvysovat

Kripkeho struktura

  • AP je množina atomic propositions (logických formulí)

  • Kripkeho struktura nad AP je trojice M = (S, R, L), kde

    • S je konečná množina stavů

    • R⊆S×SR \subseteq S \times S je transition relation taková, že pro ∀s∃s′:(s,s′)∈R\forall s \exist s' : (s, s') \in R

    • L:S→2APL : S \rightarrow 2^{AP} je labeling function

  • poznámky

    • nekonečné cesty

    • někdy množina iniciálních stavů S0

    • AP ~ Boolean variables

CTL (Computation Tree Logic)

  • A|E + X|G|F|U (next, globally, future, P until Q)

  • A - vsechny stavy, ktery ze me jdou

  • E - aspon v jednom stavu, kterej ze me jde

  • X - dalsi stav na ceste musi mit muj parametr

  • napr. EX(t) znamena, ze aspon na jednom stavu, kterej ze me jde, plati, ze nakej jeho naslednik obsahuje t

LTL (Linear Time Logic)

  • jen X|G|F|U (implicitně pro všechny cesty)

  • vnořování temporálních operátorů: X (X (G p)) = XXG p

CTL vs. LTL

  • AG(EF p) (CTL) nemá formuli v LTL (např. G(F p) není eqvivalentní)

  • FG p (LTL) nemá formuli v CTL (např. AF (AG p) není eqivalentní)

  • takze CTL a LTL jsou jinak silny (neni nic silnejsi, ale umej jiny veci)

  • CTL* umí obojí (path vs state formulas)

Materiály