Logic, Rewriting, and Concurrency

Name: Logic, Rewriting, and Concurrency | Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday

Narciso Martí-Oliet Peter Csaba Ölveczky Carolyn Talcott(Herausgeber*in)

Springer (Verlag)

Erschienen am 26. August 2015

XI, 634 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-23165-5 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Contents
José Meseguer: Scientist and Friend Extraordinaire
1 José's Origins and Positions
2 José's Research
3 José the Person and Scientist
4 José's PhD Students
References
Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
1 Introduction
2 Preliminaries
2.1 Search Tree Example
2.2 Membership Equational Logic
2.3 Unification
2.4 Rewriting Logic
2.5 Executable Rewrite Theories
2.6 Reachability Goals
2.7 Narrowing
3 Sentence-Normalized Rewriting
4 Conditional Narrowing Modulo Unification
4.1 Transformations and Calculus Rules for Unification
5 Reachability by Conditional Narrowing
5.1 Calculus Rules for Reachability
6 Example
7 Related Work, Conclusions and Future Work
References
Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis
1 Introduction
2 Rewriting Logic and Maude
2.1 Preliminaries
2.2 Rewrite Theories and Maude Modules
2.3 Rewriting and Generalization Modulo Equational Theories
3 The Assertion Language
3.1 The Assertion Logic
3.2 System and Functional Assertions
4 Enhancing Trace Slicing
5 Integrating Assertion-Checking and Trace Slicing
5.1 Dynamic Assertion-Checking
5.2 Runtime Assertion-Based Backward Trace Slicing
5.3 The ABETS system
6 Conclusions and Further Work
References
Computer Modeling in Neuroscience: From Imperative to Declarative Programming
Abstract
1 Introduction
2 Brief Survey of Imperative Models in Neuroscience
3 Declarative Model of Extinction of Fear Conditioning
3.1 Neurobiology of the Amygdala
3.2 Computational Approach Specifics
3.3 Analysis of the Model
3.4 Implications of Main Model Findings
4 New Approach in Computational Neuroscience
References
Hybrid Multirate PALS
1 Introduction
2 Preliminaries on Multirate PALS
3 Specifying Physical Environments
3.1 Controlled Physical Environments
3.2 Correlating Physical Environments
4 Hybrid Multirate PALS
4.1 Environment-Restricted Synchronous Ensembles
4.2 Realizable Transition Sequences
4.3 Hybrid Multirate PALS Distributed Models
4.4 Relating the Synchronous and Asynchronous Models
5 Verifying Invariants Using SMT Solving
5.1 Logical Representations
5.2 Local Clocks and SMT Solving
6 Concluding Remarks
References
Debits and Credits in Petri Nets and Linear Logic
1 Introduction
2 Intuitionistic Linear Logic with Mix
2.1 Simple Products and Multisets
2.2 Horn ILLmix Sequents
3 Debit Nets
4 Debit Nets as a Model of Horn ILLmix
4.1 Big-Step Semantics
4.2 Small-Step Semantics
4.3 Encoding Horn ILLmix into Debit Nets
5 Related Work and Conclusions
A Proofs
A.1 Proofs for Sect.4.1
A.2 Proofs for Sect.4.2
A.3 Proofs for Sect.4.3
References
Alice and Bob Meet Equational Theories
1 Introduction
2 Alice&Bob Protocol Notation
2.1 Overview
2.2 Messages and Message Model
2.3 Alice&Bob in Detail
3 From Equations to Rewriting Rules
3.1 Role Scripts for Protocols
3.2 Deciding Executability
3.3 Checking Received Messages
3.4 Putting It All Together
4 Automated Translation to Tamarin
5 Related Work
6 Conclusions
References
On First-Order Model-Based Reasoning
1 Introduction
2 Model-Based Reasoning in First-Order Logic
2.1 Semantic Resolution
2.2 Hypertableaux
2.3 Model-Based Transformation of Clause Sets
2.4 The Model Evolution Calculus
2.5 SGGS: Semantically-Guided Goal-Sensitive Reasoning
3 Model-Based Reasoning in First-Order Theories
3.1 Building Theory Axioms into Resolution and Superposition
3.2 Hierarchical Reasoning by Superposition
3.3 Hierarchical Reasoning in Local Theory Extensions
3.4 Beyond SMT: Satisfiability Modulo Assignment and MCsat
4 Discussion
References
A Normal Form for Stateful Connectors
1 Introduction
2 Petri Calculi
2.1 The P/T Petri Calculus
2.2 The C/E Petri Calculus
3 Nets with Boundaries
3.1 P/T Petri Nets with Boundaries
3.2 From P/T Nets with Boundaries to P/T Calculus and Back
3.3 C/E Nets with Boundaries
4 Normal Forms for Finite State P/T terms
4.1 Finite (State and Transition) Marking Graphs
4.2 Stateless, Infinitely Branching Marking Graphs
4.3 Finite State and Infinitely Branching Marking Graph
5 Normal Forms for the C/E Petri Calculus
6 Concluding Remarks
References
Enlightening Ph.D. Students with the Elegance of Logic
Abstract
1 Preface
2 My Research Direction Before Knowing Jos00E9
3 Jos00E9's Course on Formal Methods
4 Face-to-Face Discussions with Jos00E9
5 Our Collaborations After My Graduation
6 Long-Term Influence
Acknowledgement
Two Decades of Maude
1 The Origins
2 The Language
2.1 Generalized Rewrite Theories in Maude
2.2 Reflection in Maude
2.3 Maude's Formal Tools
3 The Present: Unification and Narrowing
4 The Near Future: Rewriting Modulo SMT
4.1 Maude SMT
4.2 Symbolic Analysis of Distance-Bounding Protocols
5 Pathway Logic
5.1 About Pathway Logic
5.2 Maude's Role in Pathway Logic
6 Further Ahead
References
Formal Universes
1 Introduction
2 Universalism I : Paradise Lost?
3 Universalism II : Paradise Regained?
4 Reductionism
5 Criticism
6 Rejoinder
References
When Is a Formula a Loop Invariant?
1 Introduction
2 Examples
3 Preliminaries
4 Inductive Strengthening Procedure
5 Application to Specific Logical Theories
5.1 Polynomial Equalities
5.2 Linear Arithmetic
6 k-Induction and Strengthening
6.1 Strategy Approximation (IV) Can Often Be Effective
7 Related Work
8 Conclusions
References
Generic Proof Scores for Generate & Check Method in CafeOBJ
1 Introduction
2 Preliminaries
2.1 Transition Systems
2.2 Verification of Invariant Properties
2.3 Verification of (p Leads-to q) Properties
2.4 Generate and Check for st St
2.5 Built-in Search Predicate
2.6 Generate & Check for tr Tr
2.7 Generate&Check for Verification of Invariant Properties
2.8 Generate&Check for Verification of (p Leads-to q) Properties
2.9 System and Property Specifications, and Proof Scores
3 Generic Proof Scores for Generate & Check Method
3.1 GENcases: Generating Patterns and Checking on Them
3.2 Three Parameterized Modules for Invariant Properties
3.3 Four Parameterized Modules for (p Leads-to q) Properties
4 QLOCK Specifications
4.1 QLOCK System SpecificationsThe specifications explained in this section are in the file qlock-sys.cafe on the web page.
4.2 QLOCK Property SpecificationsThe modules in this section is in the file qlock-prop.cafe unless otherwise stated.
4.3 Extended State (State % Aid) and Possible Inductive Invariants
5 QLOCK Proof Scores
5.1 Proof Scores for Invariant Properties
5.2 Proof Scores for (p Leads-to q) Property
6 Conclusion
6.1 Related Works
6.2 Some Features of Generic Proof Scores, Generate & Check Method, and CafeOBJ
6.3 Future Issues
References
Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
1 Introduction
2 Preliminaries
3 Minimal Non--Terminating Terms at Frozen Positions
4 Modeling the Unhiding Process Using Rules
4.1 A New Notion of Minimal Non--terminating Term
5 From Minimal Terms to the CS-DP Framework
5.1 Context-Sensitive Dependency Pair Framework
6 Usable Rules in the CS-DP Framework
6.1 Strongly Minimal Terms
6.2 Left-Linearity and -Conservativity
6.3 Extended Basic CS Usable Rules
7 Experimental Evaluation
8 Conclusions
References
Model-Checking HELENA Ensembles with Spin
1 Introduction
2 Foundations on LTLX Preservation
3 The Helena Approach
4 HelenaLight
4.1 Syntax of HelenaLight Ensemble Specifications
4.2 Semantics of HelenaLight Ensemble Specifications
4.3 LTL for HelenaLight
5 PromelaLight
5.1 Syntax of PromelaLight Specifications
5.2 Semantics of PromelaLight Specifications
5.3 LTL for PromelaLight
6 Translation of HelenaLight to PromelaLight
7 -Stutter Equivalence of the Translation
8 Model-Checking HelenaLight with Spin
9 Conclusion
References
Modularity of Ontologies in an Arbitrary Institution
1 Introduction
2 Institutions
3 Conservative Extensions and Inseparability
4 Module Notions
5 Conclusions
References
Rewriting Strategies and Strategic Rewrite Programs
1 Introduction
2 Historical Considerations
3 What are Strategic Rewriting and Strategic Programs?
3.1 Rewriting
3.2 Strategic Rewrite Programs
3.3 Abstract Reduction System
3.4 Strategic Rewriting
4 Strategy Description: Different Points of View
4.1 Rewriting Logic
4.2 Rewriting Calculus
4.3 Extensional Strategies
4.4 Intensional Strategies
4.5 Positional Strategies
5 Strategy Languages
6 Operational Semantics of Strategic Programs
7 Properties of Strategic Rewriting
8 Conclusion and Further Work
References
Network-on-Chip Firewall: Countering Defective and Malicious System-on-Chip Hardware
1 Introduction
2 Background
3 Threat Model
4 Core-Based Isolation
5 NoCF Interposer Design
6 Prototype Implementation
7 Constraining a Malicious GPU
8 Formal Analysis
8.1 Analysis Overview
8.2 Formalization Details
8.3 Analysis Results
8.4 Analysis Discussion
9 Related Work
10 Conclusion
References
Discretionary Information Flow Control for Interaction-Oriented Specifications
1 Introduction
2 Applications: Protocols, Services and HPC
2.1 An Identity-Secured Data Providing Service
2.2 A Binary Parallel Map-Reduce Computation
3 Choreographic Specifications of Concurrent Systems
4 Information Flows in Choreographies
5 Typing Choreographies
6 Related Works and Conclusion
A Graphs with Interfaces
References
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
1 Introduction
2 Preliminaries
2.1 Matching Logic
2.2 Reachability Logic
2.3 Rewrite Theories
3 Derivatives of ML and RL Formulas
4 A Procedure for Verifying RL Properties
5 Reachability Properties for Rewrite Theories
6 Verifying RL Properties of a Communication Protocol
7 Conclusion and Future Work
References
Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later
1 Introduction
2 Overview of the Dolev-Yao Model
3 Revisiting the Old Questions
3.1 Open-Ended Protocols
3.2 Applications and Threats from the Early Twenty-First Century
3.3 High Fidelity
3.4 Composability
3.5 Getting it into the Real World
4 Some New Issues and Trends
4.1 Privacy and Symbolic Indistinguishability
4.2 Security APIs
4.3 Multi-channel Protocols, Ceremonies, and Procedures
4.4 Combining Models and Proof Methods
5 Conclusion
References
A Denotational Semantic Theory of Concurrent Systems
1 Introduction
2 Basic Concepts
2.1 Event and Trace
2.2 Prefix Order Over Traces
2.3 Prefix Closure
2.4 Specification
3 Transformer
3.1 Trace-Wise Transformer
3.2 Smooth Transformer
3.3 Some Elementary Smooth Transformers
3.4 Fairness
3.5 Shared Resource
4 Treatment of Recursion
4.1 Classical Treatment of Recursion
4.2 Upward-Closure
4.3 Bismooth Transformer
4.4 Least Upward-Closed Fixed Point Theorem
4.5 Min-Max Fixed Points of Smooth Transformers
4.6 Fixed Point Under Fairness
5 Concluding Remarks
References
Weak Bisimulation as a Congruence in MSOS
1 Introduction
2 Background
2.1 SOS
2.2 Bisimulation and Rule Formats
2.3 Modular SOS
2.4 MSOS Terms
2.5 MSOS Labels
2.6 MSOS Rules and Specifications
2.7 Models of MSOS Specifications
2.8 Equivalence in MSOS
3 Absorbing Unobservable Transitions
4 A WB Cool MSOS Format
4.1 Positive GSOS for MSOS
4.2 Simply WB Cool MSOS
5 Conclusion
References
Satisfiability of Constraint Specifications on XML Documents
1 Introduction
2 Basic Definitions and Notation
2.1 Documents and Patterns
2.2 Pattern Morphisms and Pattern Models
3 Constraints, Clauses and Specifications
3.1 Constraints and Clauses
3.2 Specifications
3.3 Superposition of Patterns
4 Tableau-Based Reasoning for XML-patterns
5 Soundness and Completeness of the Tableau Method
6 Related Work
7 Conclusion and Further Work
References
Algebraic Reinforcement Learning Using Term Generalization
1 Introduction
2 Preliminaries
2.1 TG Learning
2.2 ACUOS
3 Algebraic Reinforcement Learning
3.1 Algebraic Regression Trees
3.2 Example Domain Specification
3.3 Hypothesis Induction with ACUOS
4 Experimental Results
4.1 Experimental Setup
4.2 Results and Discussion
5 Related Work
6 Conclusion and Further Work
References
The Formal System of Dijkstra and Scholten
1 Introduction
2 Preliminaries
3 The Propositional Fragment
4 The First-Order System
5 Derivations, Notation, and Equality
5.1 Derivations
5.2 Quantifier Notation
5.3 Equality
6 Concluding Remarks
References
From Rewriting Logic, to Programming Language Semantics, to Program Verification
1 Introduction
2 From Rewriting Logic to Language Semantics
3 From Language Semantics to Program Verification
4 Additional Related Work
5 Conclusion
References
ICEMAN: A Practical Architecture for Situational Awareness at the Network Edge
1 Introduction
2 Related Work
3 Architecture
3.1 Declarative Attribute-Based Naming
3.2 Content Dissemination
3.3 Content- and Utility-Based Caching
3.4 Network Coding and Fragmentation
3.5 Security
4 Summary of Evaluation
5 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken