Message-ID: <4E06A937DADC3842ACE4D3A1096A9EAC03831D@JANUS.eecs.berkeley.edu> From: George Necula <necula@EECS.Berkeley.EDU> Subject: Dave Schmidt talk 10/1 Date: Tue, 25 Sep 2001 09:18:39 -0700 Hi, Dave Schmidt (http://www.cis.ksu.edu/~schmidt/home.html) from Kansas State will be visiting us on October 1-3 (Mon-Wed). On Monday at 4pm he will give a Programming Systems seminar talk whose title and abstract I include below. On Tuesday at 11am he will give an invited lecture in Alex Aiken's "Topics in Software Engineering". The topic will be UML. If you want to meet him please let me know. George. =============== >From Trace Sets to Modal-Transition Systems by Stepwise Abstract Interpretation David Schmidt Kansas State University Following and expanding upon the methodology proposed by Cousot and Cousot, this presentation uses stepwise abstract interpretation to transform a system's naive trace-set semantics into formats that are readily analyzable by various temporal logics. First, a state-based abstract interpretation transforms a concrete trace-set semantics into an abstracted trace-set semantics such that linear-time properties are soundly (and in some cases, completely) preserved by LTL. Next, the trace-set semantics is abstracted into a state-set semantics by means of universal and existential abstractions: LTL is abstracted into ACTL (by the universal abstraction) and also into ECTL (by the existential abstraction); soundness and completeness conditions are stated. Finally, the desire to combine universal and existential abstractions in a single logic produces CTL*--which abstracts into the modal-mu calulus---and motivates mixed- and modal-transition systems as models, where two transition systems are used: one tracks universal behaviors and one tracks existential behaviors.
This archive was generated by hypermail 2b30 : 11/04/02 PST