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
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2006 | Buch

On Finite Alphabets and Infinite Bases II: Completed and Ready Simulation Kapitel lesen Erstes Kapitel lesen

Foundations of Software Science and Computation Structures

9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006. Proceedings

herausgegeben von: Luca Aceto, Anna Ingólfsdóttir

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch


This book constitutes the refereed proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006, held in Vienna, Austria in March 2006 as part of ETAPS.

The 28 revised full papers presented together with 1 invited paper were carefully reviewed and selected from 107 submissions. The papers are organized in topical sections on mobile processes, software science, distributed computation, categorical models, real time and hybrid systems, process calculi, automata and logic, domains, lambda calculus, types, and security.

Inhaltsverzeichnis

Frontmatter

Invited Talk

On Finite Alphabets and Infinite Bases II: Completed and Ready Simulation
Abstract
We prove that the equational theory of the process algebra BCCSP modulo completed simulation equivalence does not have a finite basis. Furhermore, we prove that with a finite alphabet of actions, the equational theory of BCCSP modulo ready simulation equivalence does not have a finite basis. In contrast, with an infinite alphabet, the latter equational theory does have a finite basis.
Taolue Chen, Wan Fokkink, Sumit Nain

Mobile Processes

A Theory for Observational Fault Tolerance
Abstract
In general, faults cannot be prevented; instead, they need to be tolerated to guarantee certain degrees of software dependability. We develop a theory for fault tolerance for a distributed pi-calculus, whereby locations act as units of failure and redundancy is distributed across independently failing locations. We give formal definitions for fault tolerant programs in our calculus, based on the well studied notion of contextual equivalence. We then develop bisimulation proof techniques to verify fault tolerance properties of distributed programs and show they are sound with respect to our definitions for fault tolerance.
Adrian Francalanza, Matthew Hennessy
Smooth Orchestrators
Abstract
A smooth orchestrator is a process with several alternative branches, every one defining synchronizations among co-located channels. Smooth orchestrators constitute a basic mechanism that may express standard workflow patterns in Web services as well as common synchronization constructs in programming languages. Smooth orchestrators may be created in one location and migrated to a different one, still not manifesting problems that usually afflict generic mobile agents.
We encode an extension of Milner’s (asynchronous) pi calculus with join patterns into a calculus of smooth orchestrators and we yield a strong correctness result (full abstraction) when the subjects of the join patterns are co-located. We also study the translation of smooth orchestrators into finite-state automata, therefore addressing the implementation of co-location constraints and the case when synchronizations are not linear with respect to subjects.
Cosimo Laneve, Luca Padovani
On the Relative Expressive Power of Asynchronous Communication Primitives
Abstract
In this paper, we study eight asynchronous communication primitives, arising from the combination of three features: arity (monadic vs polyadic data), communication medium (message passing vs shared dataspaces) and pattern-matching. Each primitive has been already used in at least one language appeared in literature; however, to uniformly reason on such primitives, we plugged them in a common framework inspired by the asynchronous π-calculus. By means of possibility/impossibility of ‘reasonable’ encodings, we compare every pair of primitives to obtain a hierarchy of languages based on their relative expressive power.
Daniele Gorla
More on Bisimulations for Higher Order π-Calculus
Abstract
In this paper, we prove the coincidence between strong/weak context bisimulation and strong/weak normal bisimulation for higher order π-calculus, which generalizes Sangiorgi’s work. To achieve this aim, we introduce indexed higher order π-calculus, which is similar to higher order π-calculus except that every prefix of any process is assigned to indices. Furthermore we present corresponding indexed bisimulations for this calculus, and prove the equivalence between these indexed bisimulations. As an application of this result, we prove the equivalence between strong/weak context bisimulation and strong/weak normal bisimulation.
Zining Cao

Software Science

Register Allocation After Classical SSA Elimination is NP-Complete
Abstract
Chaitin proved that register allocation is equivalent to graph coloring and hence NP-complete. Recently, Bouchez, Brisk, and Hack have proved independently that the interference graph of a program in static single assignment (SSA) form is chordal and therefore colorable in linear time. Can we use the result of Bouchez et al. to do register allocation in polynomial time by first transforming the program to SSA form, then performing register allocation, and finally doing the classical SSA elimination that replaces φ-functions with copy instructions? In this paper we show that the answer is no, unless P = NP: register allocation after classical SSA elimination is NP-complete. Chaitin’s proof technique does not work for programs after classical SSA elimination; instead we use a reduction from the graph coloring problem for circular arc graphs.
Fernando Magno Quintão Pereira, Jens Palsberg
A Logic of Reachable Patterns in Linked Data-Structures
Abstract
We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the neighborhood of a node that is reachable via a regular expression from a designated node. The logic is closed under boolean operations (entailment, negation) and has a finite model property. The key technical result is the proof of decidability.
We show how to express precondition, postconditions, and loop invariants for some interesting programs. It is also possible to express properties such as disjointness of data-structures, and low-level heap mutations. Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number of pointer fields. The latter provides a way to naturally specify postconditions that relate the fields on entry to a procedure to the fields on exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations.
Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani

Distributed Computation

Dynamic Policy Discovery with Remote Attestation
Abstract
Remote attestation allows programs running on trusted hardware to prove their identity (and that of their environment) to programs on other hosts. Remote attestation can be used to address security concerns if programs agree on the meaning of data in attestations. This paper studies the enforcement of code-identity based access control policies in a hostile distributed environment, using a combination of remote attestation, dynamic types, and typechecking. This ensures that programs agree on the meaning of data and cannot violate the access control policy, even in the presence of opponent processes. The formal setting is a π-calculus with secure channels, process identity, and remote attestation. Our approach allows executables to be typechecked and deployed independently, without the need for secure initial key and policy distribution beyond the trusted hardware itself.
Corin Pitcher, James Riely
Distributed Unfolding of Petri Nets
Abstract
Some recent Petri net-based approaches to fault diagnosis of distributed systems suggest to factor the problem into local diagnoses based on the unfoldings of local views of the system, which are then correlated with diagnoses from neighbouring supervisors. In this paper we propose a notion of system factorisation expressed in terms of pullback decomposition. To ensure coherence of the local views and completeness of the diagnosis, data exchange among the unfolders needs to be specified with care. We introduce interleaving structures as a format for data exchange between unfolders and we propose a distributed algorithm for computing local views of the unfolding for each system component. The theory of interleaving structures is developed to prove correctness of the distributed unfolding algorithm.
Paolo Baldan, Stefan Haar, Barbara König
On the μ-Calculus Augmented with Sabotage
Abstract
We study logics and games over dynamically changing structures. Van Benthem’s sabotage modal logic consists of modal logic with a cross-model modality referring to submodels from which a transition has been removed. We add constructors for forming least and greatest monadic fixed-points to that logic and obtain the sabotage μ-calculus. We introduce backup parity games as an extension of standard parity games where in addition, both players are able to delete edges of the arena and to store, resp., restore the current appearance of the arena by use of a fixed number of registers. We show that these games serve as model checking games for the sabotage μ-calculus, even if the access to registers follows a stack discipline. The problem of solving the games with restricted register access turns out to be PSPACE-complete while the more general games without a limited access become EXPTIME-complete (for at least three registers).
Philipp Rohde

Categorical Models

A Finite Model Construction for Coalgebraic Modal Logic
Abstract
In recent years, a tight connection has emerged between modal logic on the one hand and coalgebras, understood as generic transition systems, on the other hand. Here, we prove that (finitary) coalgebraic modal logic has the finite model property. This fact not only reproves known completeness results for coalgebraic modal logic, which we push further by establishing that every coalgebraic modal logic admits a complete axiomatization of rank 1; it also enables us to establish a generic decidability result and a first complexity bound. Examples covered by these general results include, besides standard Hennessy-Milner logic, graded modal logic and probabilistic modal logic.
Lutz Schröder
Presenting Functors by Operations and Equations
Abstract
We take the point of view that, if transition systems are coalgebras for a functor T, then an adequate logic for these transition systems should arise from the ‘Stone dual’ L of T. We show that such a functor always gives rise to an ‘abstract’ adequate logic for T-coalgebras and investigate under which circumstances it gives rise to a ‘concrete’ such logic, that is, a logic with an inductively defined syntax and proof system. We obtain a result that allows us to prove adequateness of logics uniformly for a large number of different types of transition systems and give some examples of its usefulness.
Marcello M. Bonsangue, Alexander Kurz
Bigraphical Models of Context-Aware Systems
Abstract
As part of ongoing work on evaluating Milner’s bigraphical reactive systems, we investigate bigraphical models of context-aware systems, a facet of ubiquitous computing. We find that naively encoding such systems in bigraphs is somewhat awkward; and we propose a more sophisticated modeling technique, introducing Plato-graphical models, alleviating this awkwardness. We argue that such models are useful for simulation and point out that for reasoning about such bigraphical models, the bisimilarity inherent to bigraphical reactive systems is not enough in itself; an equivalence between the bigraphical reactive systems themselves is also needed.
L. Birkedal, S. Debois, E. Elsborg, T. Hildebrandt, H. Niss
Processes for Adhesive Rewriting Systems
Abstract
Rewriting systems over adhesive categories have been recently introduced as a general framework which encompasses several rewriting-based computational formalisms, including various modelling frameworks for concurrent and distributed systems. Here we begin the development of a truly concurrent semantics for adhesive rewriting systems by defining the fundamental notion of process, well-known from Petri nets and graph grammars. The main result of the paper shows that processes capture the notion of true concurrency—there is a one-to-one correspondence between concurrent derivations, where the sequential order of independent steps is immaterial, and (isomorphism classes of) processes. We see this contribution as a step towards a general theory of true concurrency which specialises to the various concrete constructions found in the literature.
Paolo Baldan, Andrea Corradini, Tobias Heindel, Barbara König, Paweł Sobociński

Real Time and Hybrid Systems

On Metric Temporal Logic and Faulty Turing Machines
Abstract
Metric Temporal Logic (MTL) is a real-time extension of Linear Temporal Logic that was proposed fifteen years ago and has since been extensively studied. Since the early 1990s, it has been widely believed that some very small fragments of MTL are undecidable (i.e., have undecidable satisfiability and model-checking problems). We recently showed that, on the contrary, some substantial and important fragments of MTL are decidable [19,20]. However, until now the question of the decidability of full MTL over infinite timed words remained open.
In this paper, we settle the question negatively. The proof of undecidability relies on a surprisingly strong connection between MTL and a particular class of faulty Turing machines, namely ‘insertion channel machines with emptiness-testing’.
Joël Ouaknine, James Worrell
Denotational Semantics of Hybrid Automata
Abstract
We introduce a denotational semantics for non-linear hybrid automata, and relate it to the operational semantics given in terms of hybrid trajectories. The semantics is defined as least fixpoint of an operator on the continuous domain of functions of time that take values in the lattice of compact subsets of n-dimensional Euclidean space. The semantic function assigns to every point in time the set of states the automaton can visit at that time, starting from one of its initial states. Our main results are the correctness and computational adequacy of the denotational semantics with respect to the operational semantics and the fact that the denotational semantics is computable.
Abbas Edalat, Dirk Pattinson

Process Calculi

Reversing Algebraic Process Calculi
Abstract
Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, and even programming languages for quantum computing. We formulate a procedure for converting operators of standard algebraic process calculi such as CCS, ACP and CSP into reversible operators, while preserving their operational semantics.
Iain Phillips, Irek Ulidowski
Conjunction on Processes: Full–Abstraction Via Ready–Tree Semantics
Abstract
A key problem in mixing operational (e.g., process–algebraic) and declarative (e.g., logical) styles of specification is how to deal with inconsistencies arising when composing processes under conjunction. This paper introduces a conjunction operator on labelled transition systems capturing the basic intuition of “a and b = false”, and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation.
The main body of the paper is concerned with characterising the largest precongruence contained in the naive preorder. This characterisation will be based on a novel semantics called ready–tree semantics, which refines ready traces but is coarser than ready simulation. It is proved that the induced ready–tree preorder is compositional and fully–abstract, and that the conjunction operator indeed reflects conjunction.
The paper’s results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and temporal logics.
Gerald Lüttgen, Walter Vogler
Undecidability Results for Bisimilarity on Prefix Rewrite Systems
Abstract
We answer an open question related to bisimilarity checking on labelled transition systems generated by prefix rewrite rules on words. Stirling (1996, 1998) proved the decidability of bisimilarity for normed pushdown processes. This result was substantially extended by Sénizergues (1998, 2005) who showed the decidability for regular (or equational) graphs of finite out-degree (which include unnormed pushdown processes). The question of decidability of bisimilarity for a more general class of so called Type -1 systems (generated by prefix rewrite rules of the form \(R\,{\mathop{\longrightarrow}\limits^{a}}\,w\) where R is a regular language) was left open; this was repeatedly indicated by both Stirling and Sénizergues. Here we answer the question negatively, i.e., we show undecidability of bisimilarity on Type -1 systems, even in the normed case. We complete the picture by considering classes of systems that use rewrite rules of the form \(w\,{\mathop{\longrightarrow}\limits^{a}}\,R\) and \(R_{1}\,{\mathop{\longrightarrow}\limits^{a}}\,R_{2}\) and show when they yield low undecidability (Π\(^{\rm 0}_{\rm 1}\)-completeness) and when high undecidability (Σ\(^{\rm 1}_{\rm 1}\)-completeness), all with and without the assumption of normedness.
Petr Jančar, Jiří Srba

Automata and Logic

Propositional Dynamic Logic with Recursive Programs
Abstract
We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs.
Christof Löding, Olivier Serre
A Semantic Approach to Interpolation
Abstract
Interpolation results are investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation, we generate, prove and classify a series of interpolation results for first-order logic. A few of these results non-trivially generalize known interpolation results. All the others are new.
Andrei Popescu, Traian Florin Şerbănuţă, Grigore Roşu
First-Order and Counting Theories of ω-Automatic Structures
Abstract
The logic \({\mathcal L}({\mathcal Q}_u)\) extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying ... belongs to the set C”). This logic is investigated for structures with an injective ω-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [4]. It is shown that, as in the case of automatic structures [13], also modulo-counting quantifiers as well as infinite cardinality quantifiers (“there are \(\varkappa\) many elements satisfying ...”) lead to decidable theories. For a structure of bounded degree with injective ω-automatic presentation, the fragment of \({\mathcal L}({\mathcal Q}_u)\) that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (ω-automaticity and bounded degree) are necessary for this result to hold.
Dietrich Kuske, Markus Lohrey
Parity Games Played on Transition Graphs of One-Counter Processes
Abstract
We consider parity games played on special pushdown graphs, namely those generated by one-counter processes. For parity games on pushdown graphs, it is known from [23] that deciding the winner is an ExpTime-complete problem. An important corollary of this result is that the μ-calculus model checking problem for pushdown processes is ExpTime-complete. As one-counter processes are special cases of pushdown processes, it follows that deciding the winner in a parity game played on the transition graph of a one-counter process can be achieved in ExpTime. Nevertheless the proof for the ExpTime-hardness lower bound of [23] cannot be adapted to that case. Therefore, a natural question is whether the ExpTime upper bound can be improved in this special case. In this paper, we adapt techniques from [11,4] and provide a PSpace upper bound and a DP-hard lower bound for this problem. We also give two important consequences of this result. First, we improve the best upper bound known for model-checking one-counter processes against μ-calculus. Second, we show how these games can be used to solve pushdown games with winning conditions that are Boolean combinations of a parity condition on the control states with conditions on the stack height.
Olivier Serre

Domains, Lambda Calculus, Types

Bidomains and Full Abstraction for Countable Nondeterminism
Abstract
We describe a denotational semantics for a sequential functional language with random number generation over a countably infinite set (the natural numbers), and prove that it is fully abstract with respect to may-and-must testing.
Our model is based on biordered sets similar to Berry’s bidomains, and stable, monotone functions. However, (as in prior models of unbounded non-determinism) these functions may not be continuous. Working in a biordered setting allows us to exploit the different properties of both extensional and stable orders to construct a Cartesian closed category of sequential, discontinuous functions, with least and greatest fixpoints having strong enough properties to prove computational adequacy.
We establish full abstraction of the semantics by showing that it contains a simple, first-order “universal type-object” within which all types may be embedded using functions defined by (countable) ordinal induction.
James Laird
An Operational Characterization of Strong Normalization
Abstract
This paper introduces the Φ-calculus, a new call-by-value version of the λ-calculus, following the spirit of Plotkin’s λβ v -calculus. The Φ-calculus satisfies some interesting properties, in particular that its set of solvable terms coincides with the set of β-strongly normalizing terms in the classical λ-calculus.
Luca Paolini, Elaine Pimentel, Simona Ronchi Della Rocca
On the Confluence of λ-Calculus with Conditional Rewriting
Abstract
The confluence of untyped λ-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of λ-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty’s result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.
Frédéric Blanqui, Claude Kirchner, Colin Riba

Security

Guessing Attacks and the Computational Soundness of Static Equivalence
Abstract
The indistinguishability of two pieces of data (or two lists of pieces of data) can be represented formally in terms of a relation called static equivalence. Static equivalence depends on an underlying equational theory. The choice of an inappropriate equational theory can lead to overly pessimistic or overly optimistic notions of indistinguishability, and in turn to security criteria that require protection against impossible attacks or—worse yet—that ignore feasible ones. In this paper, we define and justify an equational theory for standard, fundamental cryptographic operations. This equational theory yields a notion of static equivalence that implies computational indistinguishability. Static equivalence remains liberal enough for use in applications. In particular, we develop and analyze a principled formal account of guessing attacks in terms of static equivalence.
Martín Abadi, Mathieu Baudet, Bogdan Warinschi
Handling exp,× (and Timestamps) in Protocol Analysis
Abstract
We present a static analysis technique for the verification of cryptographic protocols, specified in a process calculus. Rather than assuming a specific, fixed set of cryptographic primitives, we only require them to be specified through a term rewriting system, with no restrictions. Examples are provided to support our analysis. First, we tackle forward secrecy for a Diffie-Hellman-based protocol involving exponentiation, multiplication and inversion. Then, a simplified version of Kerberos is analyzed, showing that its use of timestamps succeeds in preventing replay attacks.
Roberto Zunino, Pierpaolo Degano
Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario
Abstract
Web services are an important series of industry standards for adding semantics to web-based and XML-based communication, in particular among enterprises. Like the entire series, the security standards and proposals are highly modular. Combinations of several standards are put together for testing as interoperability scenarios, and these scenarios are likely to evolve into industry best practices. In the terminology of security research, the interoperability scenarios correspond to security protocols. Hence, it is desirable to analyze them for security. In this paper, we analyze the security of the new Secure WS-ReliableMessaging Scenario, the first scenario to combine security elements with elements of another quality-of-service standard. We do this both symbolically and cryptographically. The results of both analyses are positive. The discussion of actual cryptographic primitives of web services security is a novelty of independent interest in this paper.
Michael Backes, Sebastian Mödersheim, Birgit Pfitzmann, Luca Viganò
Backmatter
Metadaten
Titel
Foundations of Software Science and Computation Structures
herausgegeben von
Luca Aceto
Anna Ingólfsdóttir
Copyright-Jahr
2006
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-33046-2
Print ISBN
978-3-540-33045-5
DOI
https://doi.org/10.1007/11690634

Premium Partner

    Bildnachweise