Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben

2002 | Buch

Semantical Evaluations as Monadic Second-Order Compatible Structure Transformations Kapitel lesen Erstes Kapitel lesen

Foundations of Software Science and Computation Structures

5th International Conference, FOSSACS 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings

herausgegeben von: Mogens Nielsen, Uffe Engberg

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

ETAPS 2002 is the ?fth instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference that was established in 1998by combining a number of existing and new conferences. This year it comprises ?ve conferences (FOSSACS, FASE, ESOP, CC, TACAS), thirteen satellite workshops (ACL2, AGT, CMCS, COCV, DCC, INT, LDTA, SC, SFEDL, SLAP, SPIN, TPTS and VISS), eight invited lectures (not including those that are speci?c to the satellite events), and several tutorials. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis and improvement. The languages, methodologies and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented, with an inclination towards theory with a practical motivation on one hand and soundly-based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware systems, and the emphasis on software is not intended to be exclusive.

Inhaltsverzeichnis

Frontmatter

Invited Paper

Semantical Evaluations as Monadic Second-Order Compatible Structure Transformations
Abstract
A transformation of structures τ is monadic second-order compatible (MS-compatible) if every monadicsec ond-order property P can be effectively rewritten into a monadic second-order property Q such that, for every structure S, if T is the transformed structure τ (S), then P(T) holds i. Q(S) holds.
We will review Monadic Second-order definable transductions (MS-transductions): they are MS-compatible transformations of a particular form, i.e., defined by monadicsec ond-order (MS) formulas.
The unfolding of a directed graph into a tree is an MS-compatible transformation that is not an MS-transduction.
The MS-compatibility of various transformations of semantical interest follows. We will present three main cases and discuss applications and open problems.
Bruno Courcelle

Contributed Papers

Verification for Java’s Reentrant Multithreading Concept
Abstract
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model offers coordination via lock-synchronization, and communication by synchronous message passing, including re-entrant method calls, and by instance variables shared amongthreads.
To reason about multithreaded programs, we introduce in this paper an assertional proof method for Java MT (“Multi-Threaded Java”), a small concurrent sublanguage of Java, coveringthe mentioned concurrency issues as well as the object-based core of Java, i.e., object creation, side effects, and aliasing, but leaving aside inheritance and subtyping.
Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen
On the Integration of Observability and Reachability Concepts
Abstract
This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework.We develop the essential notions that are needed to construct an institution which takes into account both the generation- and observation-oriented aspects ofsof tware systems. Thereby the underlying paradigm is that the semantics ofa specification should be as loose as possible to capture all its correct realizations. We also consider the so-called “idealized models” ofa specification which are useful to study the behavioral properties a user can observe when he/she is experimenting with the system. Finally, we present sound and complete proofsystems that allow us to derive behavioral properties from the axioms of a given specification.
Michel Bidoit, Rolf Hennicker
Proving Correctness of Timed Concurrent Constraint Programs
Abstract
A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on modalities which allow one to specify what a process produces as a reaction to what its environment inputs. These modalities provide an assumption/commitment style of specification which allows a sound and complete compositional axiomatization of the reactive behavior of timed concurrent constraint programs.
Frank S. de Boer, Maurizio Gabbrielli, Maria Chiara Meo
Generalised Regular MSC Languages
Abstract
We establish the concept of regularity for languages consisting of Message Sequence Charts (MSCs). To this aim, we formalise their behaviour by string languages and give a natural de.nition of regularity in terms of an appropriate Nerode right congruence. Moreover, we present a class of accepting automata and establish several decidability and closure properties of MSC languages. We also provide a logical characterisation by a monadic second-order logic interpreted over MSCs. In contrast to existing work on regular MSC languages, our approach is neither restricted to a certain class of MSCs nor tailored to a fixed communication medium (such as a FIFO channel). It explicitly allows MSCs with message overtaking and is thus applicable to a broad range of channel types like mixtures of stacks and FIFOs.
Benedikt Bollig, Martin Leucker, Thomas Noll
On Compositional Reasoning in the Spi-calculus
Abstract
Observational equivalences can be used to reason about the correctness of security protocols described in the spi-calculus. Unlike in CCS or in Π-calculus, these equivalences do not enjoy a simple formulation in spi-calculus. The present paper aims at enriching the set of tools for reasoning on processes by providing a few equational laws for a sensible notion of spi-bisimilarity. We discuss the dificulties underlying compositional reasoning in spi-calculus and show that, in some cases and with some care, the proposed laws can be used to build compositional proofs. A selection of these laws forms the basis of a proof system that we show to be sound and complete for the strong version of bisimilarity.
Michele Boreale, Daniele Gorla
On Specification Logics for Algebra-Coalgebra Structures: Reconciling Reachability and Observability
Abstract
The paper builds on recent results regarding the expressiveness of modal logics for coalgebras in order to introduce a specification framework for coalgebraic structures which offers support for modular specification. An equational specification framework for algebraic structures is obtained in a similar way. The two frameworks are then integrated in order to account for structures comprising both a coalgebraic (observational) component and an algebraic (computational) component. The integration results in logics whose sentences are either coalgebraic (modal) or algebraic (equational) in nature, but whose associated notions of satisfaction take into account both the coalgebraic and the algebraic features of the structures being specified. Each of the logics thus obtained also supports modular specification.
Corina Cîrstea
A First-Order One-Pass CPS Transformation
Abstract
We present a new transformation of call-by-value lambdaterms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation. This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.
Olivier Danvy, Lasse R. Nielsen
The Demonic Product of Probabilistic Relations
Abstract
The demonic product of two probabilistic relations is defined and investigated. It is shown that the product is stable under bisimulations when the mediating object is probabilistic,and that under some mild conditions the non-deterministic fringe of the probabilistic relations behaves properly: the fringe of the product equals the demonic product of the fringes.
Ernst-Erich Doberkat
Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation
Abstract
We address the problem of minimizing labelled transition systems for name passing calculi. We show how the co-algebraic formulation of automata with naming directlysuggests an effective minimization algorithm which reduces the number of states to be analyzed in the verification of properties for name passing process calculi.
Gianluigi Ferrari, Ugo Montanari, Marco Pistore
Varieties of Effects
Abstract
We introduce the notion of effectoid as a way of axiomatising the notion of “computational effect”. Guided by classical algebra, we define several effectoids equationally and explore their relationship with each other. We demonstrate their computational relevance by applying them to global exceptions, partiality, continuations, and global state.
Carsten Führmann
A Characterization of Families of Graphs in Which Election Is Possible
Extended Abstract
Abstract
The Model. We consider networks of processors with arbitrary topology. A network is represented as a connected, undirected graph where vertices denote processors and edges denote direct communication links. Labels (or states) are attached to vertices and edges. Labels are modified locally, that is, on a subgraph of fixed radius 1 of the given graph, according to certain rules depending on the subgraph only (local computations). The relabelling is performed until no more transformation is possible, i.e., until a normal form is obtained.
The Problem. The election problem is one of the paradigms of the theory of distributed computing. Considering a network of processors the election problem is to arrive at a configuration where exactly one process is in the state elected and all other processes are in the state non-elected see [Tel00]. The elected vertex is used to make decisions, to centralize or to broadcast some information.
Known Results. Graphs where election is possible were already studied but the algorithms usually involved some particular knowledge. Solving the problem for different knowledge has been investigated for some particular cases including (see [Tel00] for details): - the network is known to be a tree - the network is known to be complete - the network is known to be a grid - the nodes have different identification numbers - the network is known to be a ring and has a known prime number of vertices.
Emmanuel Godard, Yves Métivier
Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds*
Abstract
We present a general method for proving DP-hardness of equivalencechecking problems on one-counter automata. For this we show a reduction of the Sat-Unsat problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on onecounter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero).We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions).
Petr Jančar, Antonín Kučera, Faron Moller, Zdeněk Sawa
Efficient Type Matching
Abstract
Palsberg and Zhao [17] presented an O(n 2) time algorithm for matching two recursive types. In this paper, we present an O(n log n) algorithm for the same problem. Our algorithm works by reducing the type matching problem to the well-understood problem of finding a size-stable partition of a graph. Our result may help improve systems, such as Polyspin and Mockingbird, that are designed to facilitate interoperability of software components.We also discuss possible applications of our algorithm to Java. Issues related to subtyping of recursive types are also discussed.
Somesh Jha, Jens Palsberg, Tian Zhao
Higher-Order Pushdown Trees Are Easy
Abstract
We show that the monadicsec ond-order theory of an infinite tree recognized by a higher-order pushdown automaton of any level is decidable. We also show that trees recognized by pushdown automata of level n coincide with trees generated by safe higher-order grammars of level n. Our decidability result extends the result of Courcelle on algebraic(pushdo wn of level 1) trees and our own result on trees of level 2.
Teodor Knapik, Damian Niwiński, Paweł Urzyczyn
Conflict Detection and Resolution in Access Control Policy Specifications
Abstract
Graph-based specification formalisms for Access Control (AC) policies combine the advantages of an intuitive visual framework with a rigorous semantical foundation. A security policy framework specifies a set of (constructive) rules to build the system states and sets of positive and negative (declarative) constraints to specify wanted and unwanted substates. Models for AC (e.g. role-based, lattice-based or an access control list) have been specified in this framework elsewhere. Here we address the problem of inconsistent policies within this framework. Using formal properties of graph transformations, we can systematically detect inconsistencies between constraints, between rules and between a rule and a constraint and lay the foundation for their resolutions.
Manuel Koch, Luigi V. Mancini, Francesco Parisi-Presicce
Logics Admitting Final Semantics
Abstract
A logic for coalgebras is said to admit final semantics iff— up to some technical requirements—all definable classes contain a fully abstract final coalgebra. It is shown that a logic admits final semantics iff the formulas of the logic are preserved under coproducts (disjoint unions) and quotients (homomorphicimages).
Alexander Kurz
Model Checking Fixed Point Logic with Chop
Abstract
This paper examines FLC, which is the modal μ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to the modal μ-calculus. The main focus lies on FLC’s model checking problem over finite transition systems. It is proved to be Pspace-hard. A tableau model checker is given and an upper Exptime bound is derived from it. For a fixed alternation depth FLC’s model checking problem turns out to be Pspace-complete.
Martin Lange, Colin Stirling
On Model Checking Durational Kripke Structures
Extended Abstract
Abstract
We consider quantitative model checking in durational Kripke structures (Kripke structures where transitions have integer durations) with timed temporal logics where subscripts put quantitative constraints on the time it takes before a property is satisfied.
We investigate the conditions that allow polynomial-time model checking algorithms for timed versions of CTL and exhibit an important gap between logics where subscripts of the form “= c” (exact duration) are allowed, and simpler logics that only allow subscripts of the form “≤c” or “≥ c” (bounded duration).
A surprising outcome of this study is that it provides the second example of a Δp 2-complete model checking problem.
François Laroussinie, Nicolas Markey, Philippe Schnoebelen
Model-Checking Infinite Systems Generated by Ground Tree Rewriting
Abstract
We consider infinite graphs that are generated by ground tree (or term) rewriting systems. The vertices of these graphs are trees. Thus, with a finite tree automaton one can represent a regular set of vertices. It is shown that for a regular set T of vertices the set of vertices from where one can reach (respectively, infinitely often reach) the set T is again regular. Furthermore it is shown that the problems, given a tree t and a regular set T, whether all paths starting in t eventually (respectively, infinitely often) reach T, are undecidable. We then define a logic which is in some sense a maximal fragment of temporal logic with a decidable model-checking problem for the class of ground tree rewriting graphs.
Christof Löding
Bounded MSC Communication
Abstract
Message sequence charts (MSCs) and high-level message sequence charts (HMSCs) are popular formalisms for the specification of communication protocols between asynchronous processes. An important concept in this context is the size of the communication buffers used between processes. Since real systems impose limitations on the capacity (or speed) of communication links, we ask whether a given HMSC can be implemented with respect to a given buffer size imposed by the environment. We introduce four different measures for buffer sizes and investigate for each of these measures the complexity of deciding whether a given MSC (or HMSC, or hierarchical MSC) satisfies a given bound on the buffer size. The complexity of these problems varies between the classes P, NP, and coNP.
Markus Lohrey, Anca Muscholl
The Informatic Derivative at a Compact Element
Abstract
We extend the informatic derivative to compact elements in domains. This allows one to quantitatively analyze processes which manipulate both continuous and discrete data in a uniform manner.
Keye Martin
Heterogeneous Development Graphs and Heterogeneous Borrowing
Abstract
Development graphs are a tool for dealing with structured specifications in a formal program development in order to ease the management of change and reusing proofs. Often, different aspects of a software system have to be specified in different logics, since the construction of a huge logic covering all needed features would be too complex to be feasible. Therefore, we introduce heterogeneous development graphs as a means to cope with heterogeneous specifications.
We cover both the semantics and the proof theory of heterogeneous development graphs. A proof calculus can be obtained either by combining proof calculi for the individual logics, or by representing these in some “universal” logic like higher-order logic in a coherent way and then “borrowing” its calculus for the heterogeneous language.
Till Mossakowski
Notions of Computation Determine Monads
Abstract
We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
Gordon Plotkin, John Power
A Calculus of Circular Proofs and Its Categorical Semantics
Abstract
We present a calculus of “circular proofs”: the graph underlying a proof is not a finite tree but instead it is allowed to contain a certain amount of cycles.The main challenge in developing a theory for the calculus is to define the semantics of proofs, since the usual method by induction on the structure is not available. We solve this problem by associating to each proof a system of equations - defining relations among undetermined arrows of an arbitrary category with finite products and coproducts as well as constructible initial algebras and final coalgebras - and by proving that this system admits always a unique solution.
Luigi Santocanale
Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes
Abstract
We present a sequent calculus for formally verifying modal μ-calculus properties of concurrent processes. Building on work by Dam and Gurov, the proof system contains rules for the explicit manipulation of fixed-point approximants. We develop a new syntax for approximants, incorporating, in particular, modalities for approximant modification. We make essential use of this feature to prove our main result: the sequent calculus is complete for establishing arbitrary μ-calculus properties of context-free processes.
Ulrich Schöpp, Alex Simpson
Note on the Tableau Technique for Commutative Transition Systems
Abstract
We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableaubased proof for BPP, that strong bisimilarity between any two states of such a transition system is decidable. It gives a general technique for extending decidability borders of strong bisimilarity for a wide class of in.nite-state transition systems. This is demonstrated for several process formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets.
Jiří Srba
A Semantic Basis for Local Reasoning
Abstract
We present a semantic analysis of a recently proposed formalism for local reasoning, where a specification (and hence proof) can concentrate on only those cells that a program accesses. Our main results are the soundness and, in a sense, completeness of a rule that allows frame axioms, which describe invariant properties of portions of heap memory, to be inferred automatically; thus, these axioms can be avoided when writing specifications.
Hongseok Yang, Peter O’Hearn
Linearity and Bisimulation
Abstract
We introduce a theory of weak bisimilarity for the π-calculus with linear type structure [35] in which we abstract away not only τ - actions but also non-τ actions which do not affect well-typed environments. This gives an equivalence far larger than the standard bisimilarity while retaining semantic soundness. The congruency of the bisimilarity relies on a liveness property at linear channels ensured by typing. The theory is consistently extendible to settings which involve nontermination, nondeterminism and state. As an application we develop a behavioural theory of secrecy for the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach in [20][23].
Nobuko Yoshida, Kohei Honda, Martin Berger
Backmatter
Metadaten
Titel
Foundations of Software Science and Computation Structures
herausgegeben von
Mogens Nielsen
Uffe Engberg
Copyright-Jahr
2002
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-45931-6
Print ISBN
978-3-540-43366-8
DOI
https://doi.org/10.1007/3-540-45931-6