Linked e-resources
Details
Table of Contents
Intro
Preface
Organization
Model Checking and Machine Learning Joining Forces in Uppaal (Invited Paper)
Contents
Invited Papers
Concurrency and Objects Matter! Disentangling the Fabric of Real Operational Processes to Create Digital Twins
1 Towards a Digital Twin of an Organization
2 Process Mining: A Top-Down View
3 Process Mining: A Bottom-Up View
3.1 Petri Nets
3.2 Object-Centric Partially-Ordered Event Logs
3.3 Object-Centric Petri Nets
4 Conclusion
References
Qualitative-Quantitative Reasoning: Thinking Informally About Formal Things
1 Motivation
2 Informal Insights from Formalism
The PIE Model
3 Making Decisions
Electrostatically Charged Agricultural Crop Sprays
4 Orders of Magnitude
Climate Change and Complexity
4.1 Infinitesimals and Limits
4.2 Day-to-Day Reasoning
4.3 Algorithmic Complexity
4.4 Sorting
4.5 What is Computation?
5 Knowing What to Model
Covid Serial Interval
6 Monotonic Reasoning
Change at the Shops and the Impact of Automation
7 Formalising and Visualising QQ
Allen's Interval Calculus
8 Discussion and Call to Action
References
Databases and Distributed Transactions
Some Aspects of the Database Resilience
1 Introduction
2 Preliminaries
2.1 Conjunctive Query
2.2 Parameterized Complexity
2.3 Resilience Revisited
3 Formal Characterization of the Contingency Set
4 The ``Data Complexity'' of the Resilience Problem
5 Conclusion
References
On the Correctness Problem for Serializability
1 Introduction
2 Related Work
3 Background
4 The Correctness Problem for SSR- Is Decidable
4.1 Compact Representation
4.2 Construction of Finite Automaton
5 Conclusion
References
Efficient Model Checking Methods
A Set Automaton to Locate All Pattern Matches in a Term
1 Introduction
1.1 Related Work
2 Preliminaries
3 An Example Set Automaton
4 Automaton Construction
4.1 Initial State
4.2 Function-Symbol-Position Derivatives
4.3 Derivative Partitioning
4.4 Lifting the Positions of Classes
4.5 Output Patterns
4.6 Position Labels
4.7 Summary
5 Validity of the Construction
6 Correctness of the Evaluation
6.1 Evaluation Trees
6.2 Soundness and Completeness
7 Complexity and Automaton Size
8 Future Work
References
Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs
1 Introduction
2 Preliminaries
2.1 Behavioral Model
2.2 Reachability Probability
2.3 Sparse-Matrix Representations
2.4 GPU Programming
3 Proposed Optimization Flow
3.1 Identification of the SpMV
3.2 Introducing CUDA
3.3 Basic Optimizations
3.4 Hiding Memory Latency
3.5 Profile and Evaluate
4 Experimental Evaluation
4.1 NAND Case Study
4.2 Herman Case Study
4.3 Increasing Value of N
4.4 CUSP vs cuSPARSE
4.5 Comparing GPUs
5 Conclusion
References
Preface
Organization
Model Checking and Machine Learning Joining Forces in Uppaal (Invited Paper)
Contents
Invited Papers
Concurrency and Objects Matter! Disentangling the Fabric of Real Operational Processes to Create Digital Twins
1 Towards a Digital Twin of an Organization
2 Process Mining: A Top-Down View
3 Process Mining: A Bottom-Up View
3.1 Petri Nets
3.2 Object-Centric Partially-Ordered Event Logs
3.3 Object-Centric Petri Nets
4 Conclusion
References
Qualitative-Quantitative Reasoning: Thinking Informally About Formal Things
1 Motivation
2 Informal Insights from Formalism
The PIE Model
3 Making Decisions
Electrostatically Charged Agricultural Crop Sprays
4 Orders of Magnitude
Climate Change and Complexity
4.1 Infinitesimals and Limits
4.2 Day-to-Day Reasoning
4.3 Algorithmic Complexity
4.4 Sorting
4.5 What is Computation?
5 Knowing What to Model
Covid Serial Interval
6 Monotonic Reasoning
Change at the Shops and the Impact of Automation
7 Formalising and Visualising QQ
Allen's Interval Calculus
8 Discussion and Call to Action
References
Databases and Distributed Transactions
Some Aspects of the Database Resilience
1 Introduction
2 Preliminaries
2.1 Conjunctive Query
2.2 Parameterized Complexity
2.3 Resilience Revisited
3 Formal Characterization of the Contingency Set
4 The ``Data Complexity'' of the Resilience Problem
5 Conclusion
References
On the Correctness Problem for Serializability
1 Introduction
2 Related Work
3 Background
4 The Correctness Problem for SSR- Is Decidable
4.1 Compact Representation
4.2 Construction of Finite Automaton
5 Conclusion
References
Efficient Model Checking Methods
A Set Automaton to Locate All Pattern Matches in a Term
1 Introduction
1.1 Related Work
2 Preliminaries
3 An Example Set Automaton
4 Automaton Construction
4.1 Initial State
4.2 Function-Symbol-Position Derivatives
4.3 Derivative Partitioning
4.4 Lifting the Positions of Classes
4.5 Output Patterns
4.6 Position Labels
4.7 Summary
5 Validity of the Construction
6 Correctness of the Evaluation
6.1 Evaluation Trees
6.2 Soundness and Completeness
7 Complexity and Automaton Size
8 Future Work
References
Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs
1 Introduction
2 Preliminaries
2.1 Behavioral Model
2.2 Reachability Probability
2.3 Sparse-Matrix Representations
2.4 GPU Programming
3 Proposed Optimization Flow
3.1 Identification of the SpMV
3.2 Introducing CUDA
3.3 Basic Optimizations
3.4 Hiding Memory Latency
3.5 Profile and Evaluate
4 Experimental Evaluation
4.1 NAND Case Study
4.2 Herman Case Study
4.3 Increasing Value of N
4.4 CUSP vs cuSPARSE
4.5 Comparing GPUs
5 Conclusion
References