Note: Intro -- Preface -- Organization and Committees -- General Chairs -- Advisory Board -- Program Co-chairs -- Poster Chairs -- Lightning Chairs -- Media and Publicity Chairs -- Tutorial Chairs -- Local Chairs -- Local Committee -- Publication Chair -- Submission Chair -- Web Chair -- Program Committee -- Contents -- Network Analysis -- A Software to Extract Criminal Networks from Unstructured Text in Spanish -- the Case of Peruvian Criminal Networks -- Abstract -- 1 Introduction -- 2 Related Work -- 3 Problem Statement -- 4 The Proposed Tool to Extract Criminal Networks -- 5 Analysing a Peruvian Criminal Network, the Orellana's Network -- 6 Comparison and Discussion -- 7 Conclusions, Limitations and Future Work -- References -- Analysis of the Web Graph Aggregated by Host and Pay-Level Domain -- 1 Introduction -- 2 Related Work -- 3 Datasets and Definitions -- 4 Methodology of Analysis -- 5 Analysis of the PLD Graph -- 5.1 Degree Distributions -- 5.2 Components -- 5.3 Distances and Diameters -- 6 Analysis of the Host Graph -- 7 Conclusion -- References -- Characterizing Temporal Bipartite Networks - Sequential- Versus Cross-Tasking -- 1 Introduction -- 2 Real-World Temporal Bipartite Networks -- 2.1 Dataset Description -- 2.2 Network Representation -- 2.3 Basic Network Characteristics -- 3 Quantifying the Sequential/Cross-Tasking Level -- 3.1 Relative Switch Frequency -- 3.2 Relative Distraction in Time -- 3.3 Comparison of Two Real-World Networks -- 4 Correlation Between Sequential/Cross-Tasking Level and Other Centrality Metrics -- 5 Conclusion -- References -- A General Powerful Graph Pattern Matching System for Data Analysis -- 1 Introduction -- 2 Problem Formulation and Method -- 3 Applications and Experimental Analysis -- 3.1 Highly Collaborative Groups of Researchers -- 3.2 Design Pattern Observer -- 3.3 Change Coupling -- 4 Conclusion. , References -- Spectral Measures of Distortion for Change Detection in Dynamic Graphs -- 1 Introduction -- 1.1 Related Work -- 2 Proposed Framework -- 2.1 Distortion Energies -- 2.2 Choice of Scale via Reduced Functional Space -- 2.3 An Algorithm to Compute the Spectral Distortion -- 3 Experimental Evaluation -- 3.1 Experimental Comparison and Discussion -- 4 Conclusion, Limitations and Future Work -- References -- Rich-Clubs in Preferential Attachment Networks -- 1 Introduction -- 1.1 Background -- 1.2 The G(p) Model -- 1.3 Rich Clubs -- 1.4 Related Work -- 1.5 Contributions -- 2 Technical Preliminaries -- 3 Known Bounds -- 4 Proofs of the Main Theorems -- 5 Discussion -- References -- The Impact of Indirect Connections: The Case of Food Security Problem -- Abstract -- 1 Introduction -- 2 Edge Importance Measures -- 3 The Case of Food Export/Import Network -- 4 Conclusion -- Acknowledgments -- Reference -- A Compressive Sensing Framework for Distributed Detection of High Closeness Centrality Nodes in Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Compressive Sensing/Sampling -- 2.2 Compressive Sensing over Graphs -- 3 Related Work -- 3.1 Local Closeness Metrics -- 3.2 CS-Based Methods for Data Aggregation -- 4 Proposed Method -- 4.1 Proposed Local Metric -- 4.2 Measurement Construction and Score Aggregation -- 4.3 Complexity Analysis -- 5 Experimental Evaluation -- 5.1 Datasets -- 5.2 Settings -- 5.3 Evaluation Results -- 6 Conclusion -- References -- Machine Learning and Networks -- Bringing a Feature Selection Metric from Machine Learning to Complex Networks -- 1 Introduction -- 2 Feature and Node F-Measure -- 3 Node F-Measure Applied to Artificial Networks -- 3.1 LFR Networks -- 3.2 Correlation with Centrality Measures -- 3.3 Correlation with Community Role Measures -- 4 Node F-Measure Applied to Real Networks. , 5 Conclusion and Perspectives -- References -- Multi-Net: A Scalable Multiplex Network Embedding Framework -- 1 Introduction -- 2 Related Work -- 3 Problem Formulation -- 4 Methodology -- 4.1 Learning Objective -- 4.2 Random Walks on Multiplex Network -- 5 Experiments and Results -- 5.1 Experimental Setup -- 5.2 Experiment Results -- 5.3 Evaluation on Algorithm Scalability -- 6 Discussion and Future Work -- References -- Learning Structural Node Representations on Directed Graphs -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 4 Learning Structural Node Embeddings on Directed, Weighted Graphs -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Automatic Identification of Component Roles in Software Design Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Class Diagrams -- 2.2 Network Construction -- 2.3 Network Concepts -- 2.4 Class Roles -- 3 Related Work -- 4 Approach -- 4.1 Semantic and Network Features -- 4.2 Machine Learning Model -- 5 Data -- 6 Results -- 7 Conclusion -- References -- Exploring Partially Observed Networks with Nonparametric Bandits -- 1 Introduction -- 2 Related Work -- 3 Proposed Bandit Based Probing Algorithm -- 3.1 Problem Definition -- 3.2 Calculation of Expected Reward of Candidate Nodes -- 3.3 Bandit Algorithm -- 4 Experiments -- 4.1 Data -- 4.2 Impact of Initial Sampling Algorithm -- 4.3 Algorithms -- 5 Results -- 5.1 Analysis on Synthetic Networks -- 5.2 Results on Real-World Networks -- 6 Conclusions -- References -- Explicit Feedbacks Meet with Implicit Feedbacks: A Combined Approach for Recommendation System -- 1 Introduction -- 2 Methodology -- 3 Experiments -- 4 Conclusion and Future Work -- References -- Quantum Walk Neural Networks for Graph-Structured Data -- 1 Introduction -- 2 Graph Quantum Walks -- 3 Quantum Walk Neural Networks -- 3.1 Edge Ordering -- 4 Experiments. , 4.1 Node Regression -- 4.2 Graph Classification -- 4.3 Graph Regression -- 5 Limitations -- 6 Concluding Remarks -- References -- Modeling Human Behavior -- Advertisement Allocation and Mechanism Design in Native Stream Advertising -- 1 Introduction -- 1.1 Our Contribution -- 1.2 Related Work -- 2 Native Advertising Meets Interval Scheduling -- 2.1 Hardness of Native Advertising -- 2.2 Algorithms for Native Stream Advertising -- 3 Truthful Native Advertising Mechanisms -- 3.1 Preliminaries -- 3.2 Truthfulness in Expectation -- 3.3 Deterministic Truthfulness -- 4 Conclusions -- References -- Let's Talk About Refugees: Network Effects Drive Contributor Attention to Wikipedia Articles About Migration-Related Topics -- 1 Introduction -- 1.1 Background and Further Related Work -- 2 Relational Event Models for the Wikipedia Network -- 2.1 Data -- 2.2 The Network of Past Events -- 2.3 A Framework for Modeling Dyadic, Typed Events -- 2.4 Parameter Estimation Under Sampling -- 2.5 Explanatory Variables (Statistics) -- 3 Results and Discussion -- 4 Conclusion -- References -- Understanding Behavioral Patterns in Truck Co-driving Networks -- 1 Introduction -- 2 Related Work -- 3 Network Construction -- 3.1 Truck Observation Data -- 3.2 Construction from Raw Data -- 3.3 Co-driving Network -- 3.4 Robustness Checks -- 3.5 Regional Co-driving Network -- 4 Approach -- 4.1 Network-Driven Understanding of Co-driving Behavior -- 4.2 Community-Driven Understanding of Co-driving Behavior -- 5 Results -- 5.1 Network Statistics -- 5.2 Attribute Assortativity -- 5.3 Average Maximal Community Assortativity -- 6 Conclusion -- References -- Theoretical Study of Self-organized Phase Transitions in Microblogging Social Networks -- Abstract -- 1 Introduction -- 2 Brief Theoretical Background -- 3 Three-Parameter Kinetics of the Phase Transitions -- 3.1 Self-organized Scheme. , 3.2 Kinetics of the Phase Transition -- 3.3 Stochastic Behavior of the Phase Transitions -- 4 Conclusions -- Acknowledgments -- References -- Using Active Queries to Learn Local Stochastic Behaviors in Social Networks -- 1 Introduction -- 2 Preliminaries -- 3 Inferring Probabilistic Threshold Functions -- 4 Experimental Evaluation of Our Algorithm -- 5 Future Research Directions -- References -- Networking Strategies and Efficiency in Human Communication Networks -- 1 Introduction -- 2 Developing Models of Networking Strategies -- 2.1 Structural Change Strategy -- 2.2 Frequency Change Strategy -- 3 Measuring Efficiency -- 4 Data -- 5 Results -- 5.1 Efficiency under Complementary Networking Strategies -- 5.2 Comparison with an Empirical Reconstruction of the Networking Process -- 6 Discussion -- References -- Influence, Reputation and Trust -- The Costs of Overambitious Seeding of Social Products -- 1 Introduction -- 2 The Model, the Networks, and the Simulations -- 3 Simulation Results and the Costs of Overambitious Seeding -- 3.1 Synthetic Networks -- 3.2 Simulations: Facebook Friendship Graphs -- 4 Conclusion -- References -- Procedural Influence on Consensus Formation in Social Networks -- 1 Introduction -- 2 Procedural Influence -- 3 Modelling Procedural Influence -- 3.1 A Multidimensional Model of Social Influence -- 3.2 Integrating Procedural Influence -- 4 Agent-Based Simulation -- 4.1 Model Setup and Experiment Design -- 4.2 Sensitivity Analysis -- 5 Conclusion -- References -- Peer Influence in Large Dynamic Network: Quasi-experimental Evidence from Scratch -- 1 Introduction -- 2 Methods -- 3 Results -- 3.1 Production Behaviour -- 3.2 Consumption Behaviour -- 4 Discussion -- A Appendix -- References -- Modeling the Co-evolving Polarization of Opinion and News Propagation Structure in Social Media -- 1 Introduction. , 2 Opinion Polarization Models.

Note: Intro -- Preface -- Organization and Committees -- General Chairs -- Advisory Board -- Program Co-chairs -- Poster Chairs -- Lightning Chairs -- Media and Publicity Chairs -- Tutorial Chairs -- Local Chairs -- Local Committee -- Publication Chair -- Submission Chair -- Web Chair -- Program Committee -- Contents -- Link Analysis and Ranking -- A New Group Centrality Measure for Maximizing the Connectedness of Network Under Uncertain Connectivity -- 1 Introduction -- 2 Related Work -- 3 Proposed Measure -- 3.1 Connectedness Centrality -- 3.2 Solution Algorithm -- 3.3 Group-Connectedness Centrality -- 4 Experimental Settings -- 5 Experimental Results -- 5.1 Visualization of Representatives and Their Clusters -- 5.2 Stability with Respect to the Number of Simulations -- 5.3 Reachability Under Link Cutting -- 5.4 Computation Time -- 6 Conclusion -- References -- Walk Prediction in Directed Networks -- 1 Introduction -- 2 Related Works -- 3 Proposed Model -- 3.1 Preference/Attraction Score -- 3.2 Learning the Model -- 4 Evaluation -- 4.1 Dataset -- 4.2 Baseline Methods -- 4.3 Results -- 5 Conclusions -- References -- Average-Case Behavior of k-Shortest Path Algorithms -- 1 Introduction -- 2 Related Work -- 3 Algorithms -- 3.1 Yen's Algorithm -- 3.2 Feng's Algorithm -- 4 Average-Case Analysis of Yen's Algorithm -- 4.1 Empirical Results on Average-Case Behavior of Yen's Algorithm -- 5 Average-Case Analysis of Feng's Algorithm -- 5.1 Empirical Results on Feng's Average-Case Behavior -- 6 Conclusion -- References -- Scaling of Random Walk Betweenness in Networks -- 1 Introduction -- 2 Random Walk Betweenness -- 2.1 Numerical Results -- 3 Normalized Random Walk Betweenness -- 3.1 Numerical Results -- 4 Conclusions -- References -- Fast Approximated Betweenness Centrality of Directed and Weighted Graphs -- 1 Introduction -- 2 Related Work. , 3 Fast BC Computation of Weighted and Directed Graphs -- 3.1 Notation -- 3.2 Brandes' Algorithm -- 3.3 Weighted Modularity and Louvain Method -- 3.4 W2C-FastBC -- 4 Evaluation: Dynamic Analysis of a Real-World Road Network -- 5 Conclusion -- References -- Node Ordering for Rescalable Network Summarization (or, the Apparent Magic of Word Frequency and Age of Acquisition in the Lexicon) -- 1 Introduction -- 2 The Node Ordering Problem: Approximating Degree -- 3 Related Work -- 4 Case Study: Word Recognition and the Phonological Network -- 5 Discussion and Future Directions -- References -- Systematic Biases in Link Prediction: Comparing Heuristic and Graph Embedding Based Methods -- 1 Introduction -- 2 Link Prediction Evaluation Framework -- 2.1 Creation of Learning and Prediction Sets -- 2.2 Link Prediction -- 2.3 Choice of an Appropriate Score Function -- 3 Methods Evaluation -- 3.1 Method Based on Heuristics -- 3.2 Methods Based on Graph Embeddings -- 3.3 Results -- 4 Analysis of Systematic Biases -- 4.1 Graph Distance -- 4.2 Node Degree -- 4.3 Community Structure -- 5 Discussion: Effect of Biases on Recommender Systems -- 6 Conclusion -- References -- Stability and Similarity in Networks Based on Topology and Nodes Importance -- Abstract -- 1 Introduction -- 2 Stability and Similarity of Network -- 2.1 Network Transformation -- 2.2 Nodes Similarity Using Interval Orders -- 2.3 Similarity of Network Topology -- 2.4 Stability and Similarity Measure -- 3 Empirical Application: International Migration Network -- 4 Conclusion -- Acknowledgments -- References -- Delusive PageRank in Incomplete Graphs -- 1 Introduction -- 2 Related Work -- 3 Preliminaries and Problem -- 4 The HAK Measure -- 5 Experiments -- 6 Conclusion -- References -- Centrality Maps for Moving Nodes -- 1 Introduction -- 2 Centrality Maps -- 2.1 Calculation of -- 2.2 Distribution of. , 3 Applying Centrality Maps to Vehicular Networks -- 3.1 Experimental Datasets -- 3.2 Node Centralities -- 4 Results -- 4.1 Contact Density -- 4.2 Evolution Over Time -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Core Stratification of Two-Mode Networks -- 1 Introduction -- 2 Cores -- 2.1 Preliminaries -- 2.2 Graph Cores -- 2.3 Computing Cores -- 2.4 Ordering Cores -- 3 Stratification -- 3.1 One and Two Parameters Stratification -- 4 A Two-Mode Network of Epistemological Data -- 5 Conclusion -- References -- OTARIOS: OpTimizing Author Ranking with Insiders/Outsiders Subnetworks -- 1 Introduction -- 2 Preliminaries -- 2.1 Terminology -- 2.2 Bibliometrics and PageRank -- 3 Methodology -- 3.1 Problem Description -- 3.2 OTARIOS -- 4 Results -- 4.1 Performance of OTARIOS Variants -- 5 Conclusions -- References -- Cascading Effects of Targeted Attacks on the Power Grid -- 1 Introduction -- 2 Related Work -- 3 Preliminaries and Problem Formulation -- 4 Experimental Design -- 5 Results and Discussion -- 6 Summary and Future Work -- References -- Community Structure -- A Memory-Based Label Propagation Algorithm for Community Detection -- 1 Introduction -- 2 Related Work -- 3 MemLPA: A Memory-Based Label Propagation Algorithm -- 3.1 Algorithm Description -- 3.2 Complexity -- 4 Performance Study -- 4.1 Artificial Networks -- 4.2 Real-World Networks -- 4.3 Discussion -- 5 Conclusions and Future Work -- References -- Estimating the Similarity of Community Detection Methods Based on Cluster Size Distribution -- 1 Introduction -- 2 Estimating the Similarity of Community Detection Methods -- 3 Community Detection Methods -- 4 Network Dataset -- 5 Experimental Results -- 6 Discussion and Conclusion -- References -- Links in Context: Detecting and Describing the Nested Structure of Communities in Node-Attributed Networks -- 1 Introduction. , 2 Community Detection with Node Attributes -- 3 The Links in Context Approach -- 3.1 Data Representation -- 3.2 Extension of Link Communities -- 4 Evaluation -- 4.1 General Observations -- 4.2 Characteristics of Identified Communities -- 4.3 Evaluation on Datasets with Ground Truth -- 5 Conclusion -- References -- Overlapping Communities in Bipartite Graphs -- 1 Introduction -- 2 Exemplar Study Case -- 3 Related Methods -- 3.1 Ordinary Stochastic Block Model -- 3.2 Degree Corrected Stochastic Block Model -- 3.3 Bipartite Stochastic Block Model -- 3.4 Stochastic Block Model and Overlapping Communities -- 4 Stochastic Block Model for Overlapping Communities in a Bipartite Graph -- 5 Model Reduction Cases -- 6 Experiments -- 6.1 Evaluation Function -- 6.2 Generated Examples -- 7 Conclusion -- References -- Communities as Well Separated Subgraphs with Cohesive Cores: Identification of Core-Periphery Structures in Link Communities -- 1 Introduction -- 2 Cohesion and Separation -- 3 Core-Periphery Structures in Link Sets -- 4 Experiments -- 5 Summary and Discussion -- References -- Ensemble Clustering for Graphs -- 1 Introduction -- 2 Algorithm -- 2.1 Review of Multilevel Louvain -- 2.2 ECG Algorithm -- 3 Comparison Study Revisited -- 3.1 Comparison Measures -- 3.2 Main Results -- 4 Discussion -- 4.1 Resolution Limit and Stability Issue -- 4.2 Parameter Selection -- 4.3 Detecting Community Presence -- 5 Conclusion -- References -- A Community-Aware Approach for Identifying Node Anomalies in Complex Networks -- 1 Introduction -- 2 Preliminaries and Problem Statement -- 2.1 Network Terminology -- 2.2 Problem Statement -- 3 Related Work -- 4 Approach -- 4.1 Existing Approaches -- 4.2 Proposed Approach: CADA -- 5 Data -- 5.1 Real-World Network Data Sets -- 5.2 Synthetic Network Data Sets -- 5.3 Anomaly Types -- 6 Experiments -- 6.1 Experimental Setup. , 6.2 Evaluation Metrics -- 6.3 Results on Synthetic Data -- 6.4 Results on Real-World Data -- 6.5 Discussion -- 7 Conclusions and Future Work -- References -- Is Community Detection Fully Unsupervised? The Case of Weighted Graphs -- 1 Introduction -- 2 Community Detection -- 3 Normalizing Weights -- 4 Classifying Links: Inside or Outside Communities? -- 5 Supervised Label Propagation: SLP -- 6 Conclusion and Future Work -- References -- Is it Correct to Project and Detect? Assessing Performance of Community Detection on Unipartite Projections of Bipartite Networks -- 1 Introduction -- 2 Methods -- 2.1 Bipartite Network Models -- 2.2 Unipartite Projection and Edge-Weighting Schemes -- 2.3 Community Detection and Accuracy -- 3 Results -- 4 Discussion -- References -- Bayesian Complex Network Community Detection Using Nonparametric Topic Model -- 1 Introduction -- 2 Previous Work -- 3 Random Walk and Hierarchical Dirichlet Process -- 3.1 Notations -- 3.2 Random Walk Data Generation -- 3.3 Hierarchical Dirichlet Process Topic Model -- 4 Experiments -- 4.1 Models -- 4.2 Choice of Hyperparameters -- 4.3 Data -- 4.4 Evaluation Metrics -- 4.5 Results and Comparison -- 5 Discussion -- 6 Conclusion -- References -- Detecting Latent Terrorist Communities Testing a Gower's Similarity-Based Clustering Algorithm for Multi-partite Networks -- 1 Introduction -- 2 Related Work -- 3 Data -- 4 Methodology -- 5 Results -- 6 Discussion and Future Work -- References -- GLaSS: Semi-supervised Graph Labelling with Markov Random Walks to Absorption -- 1 Introduction -- 2 Method -- 2.1 DTMC Absorption Probabilities -- 2.2 Semi-supervised Graph Labelling -- 2.3 DTMC Expected Times to Absorption -- 2.4 The Graph Labelling Semi-supervised (GLaSS) Method -- 3 Data -- 4 Results -- 4.1 Comparison to Other Methods -- 5 Discussion -- References. , Semi-supervised Overlapping Community Finding Based on Label Propagation with Pairwise Constraints.

Note: Intro -- Preface -- Contents -- Reviewers List -- Part I Model Checking -- 1 Model Checking Approach to the Analysis of Biological Systems -- 1.1 Introduction -- 1.2 Verification by Model Checking -- 1.3 Methods and Tools -- 1.3.1 Model Checking Biological Systems -- 1.3.2 Parameter Synthesis for Dynamical Systems -- 1.3.3 Digital Bifurcation Analysis -- 1.4 Case Studies -- 1.4.1 Regulation of G1/S Cell Cycle Transition -- 1.4.2 Signalling Pathways -- References -- 2 Automated Reasoning for the Synthesis and Analysis of Biological Programs -- 2.1 Introduction -- 2.2 Methodology -- 2.2.1 Abstract Boolean Networks -- 2.2.2 Switching Networks -- 2.2.3 ABN and SABN Synthesis -- 2.2.4 Analysis Procedures -- 2.3 Illustrative Examples -- 2.3.1 Stem Cell Decision-Making -- 2.3.2 Myeloid Differentiation -- 2.3.3 Epidermal Differentiation -- 2.4 Discussion -- References -- 3 Statistical Model Checking-Based Analysis of Biological Networks -- 3.1 Introduction -- 3.1.1 Related Work -- 3.1.2 Outline of the Chapter -- 3.2 Pathway Models Based on a System of ODEs -- 3.2.1 ODEs Preliminaries -- 3.2.2 Trajectories of the ODE System -- 3.3 Statistical Model Checking of ODE Dynamics -- 3.3.1 BLTL -- 3.3.2 Verifying PBLTL Formulas Using Statistical Model Checking -- 3.3.3 SMC-Based Parameter Estimation for a Single System of ODEs -- 3.4 Extension of SMC to Hybrid Automata -- 3.4.1 The Markov Chain Associated with a Hybrid Automaton -- 3.4.2 Relating the Behaviors of H and MH Using BLTL -- 3.5 Applications -- 3.5.1 SMC-Based Analysis of ODE Models -- 3.5.2 SMC-Based Analysis of Hybrid Automata Based Models -- 3.6 Discussion -- References -- 4 Models, Devices, Properties, and Verification of Artificial Pancreas Systems -- 4.1 Introduction -- 4.2 The Glucose-Insulin Regulatory System -- 4.3 Diabetes Mellitus -- 4.3.1 Treatment Strategies -- 4.4 Physiological Modeling. , 4.4.1 The Hovorka Model -- 4.4.2 The Dalla Man Model and UVA/Padova Simulator -- 4.4.3 Data-Driven Approaches -- 4.5 Control Algorithms -- 4.5.1 PID Control -- 4.5.2 MPC Control -- 4.6 Specifications -- 4.6.1 Interface Correctness -- 4.6.2 Algorithm Correctness and Performance -- 4.7 Verification and Synthesis -- 4.7.1 Verification of AP Algorithms -- 4.7.2 Simulation-Based Falsification of PID Algorithm -- 4.7.3 Verification Using Data-Driven Models -- 4.7.4 Verification of AP: Future Directions -- 4.8 Conclusion -- References -- 5 Using State Space Exploration to Determine How Gene Regulatory Networks Constrain Mutation Order in Cancer Evolution -- 5.1 Introduction -- 5.2 Qualitative Networks -- 5.3 Identifying Attractors in QNs Using Binary Decision Diagrams -- 5.3.1 Binary Decision Diagrams -- 5.3.2 Attractor identification algorithm -- 5.4 Exploring Order of Mutations -- 5.5 Results -- 5.5.1 Benchmarks -- 5.5.2 Application to a Model of ER-Negative Breast Cancer -- 5.6 Future Work -- 5.7 Conclusions -- References -- Part II Formal Methods and Logic -- 6 Set-Based Analysis for Biological Modeling -- 6.1 Introduction -- 6.2 Dynamical Systems for Biological Modeling -- 6.2.1 Historical Overview -- 6.2.2 From Continuous System Models to Hybrid System Models -- 6.2.3 Model Validation and Parameter Synthesis -- 6.3 Set-Based Analysis -- 6.3.1 Reachability Analysis -- 6.3.2 Set Image Computation by Optimization -- 6.3.3 Parameter Synthesis -- 6.4 Case Studies -- 6.4.1 Mammalian Cellular Iron Homeostasis (MCIH) Model -- 6.4.2 SIR Epidemic Model -- 6.5 Conclusion -- References -- 7 Logic and Linear Programs to Understand Cancer Response -- 7.1 Introduction -- 7.2 Regulatory and Signaling Networks as Logical Programs -- 7.2.1 Preliminary Notions -- 7.2.2 Perfect Coloring Model. , 7.2.3 Caspo for Discovering Boolean Networks distinguishing different classes of patients data -- 7.2.4 Caspo-ts for Discovering Boolean Networks Distinguishing Time-Series Data of Cell Lines -- 7.2.5 Comparison of the Three Methods -- 7.3 Linear Programming Approaches in the Context of Metabolic Network Analysis -- 7.3.1 Metabolic Networks as Linear Systems -- 7.4 Hybrid Modeling -- 7.5 Conclusion -- References -- 8 Logic-Based Formalization of System Requirements for Integrated Clinical Environments -- 8.1 Introduction -- 8.2 Related Work -- 8.3 The PVS Specification Language -- 8.4 An ICE Setting -- 8.5 Overview of ICE Requirements Formalization -- 8.5.1 Domain Identification -- 8.5.2 Requirements Formalization -- 8.6 Formalization of the ICE Communication Network -- 8.6.1 Network Structure -- 8.6.2 Network Dynamics -- 8.6.3 Requirements -- 8.7 Verification -- 8.7.1 Verification of the Surge Protocol -- 8.7.2 Interactive Proof -- 8.8 Conclusions -- References -- 9 Balancing Prescriptions with Constraint Solvers -- 9.1 Introduction -- 9.2 Context and Contribution -- 9.2.1 Example -- 9.3 Formal Model -- 9.4 Searching Optimal Solutions -- 9.4.1 Using a Theorem Prover -- 9.4.2 Using an SMT Solver -- 9.4.3 Representing Traces of Execution -- 9.4.4 Selecting the Best Traces -- 9.4.5 The Example Revisited -- 9.5 Verification -- 9.6 Conclusions -- References -- 10 Metastable Regimes and Tipping Points of Biochemical Networks with Potential Applications in Precision Medicine -- 10.1 Introduction -- 10.2 Theory: Tropical Equilibrations of Chemical Reactions Networks with Rational Rate Functions -- 10.3 Methods -- 10.3.1 Computation of Minimal Branches -- 10.3.2 Generation of Perturbed Parameter Orders -- 10.3.3 Identification of Parameter Sensitivity Scores -- 10.4 Results -- 10.4.1 Biochemical Reaction Network -- 10.4.2 Computation of Distances. , 10.4.3 TCPA Proteomics Data -- 10.4.4 CPTAC Proteomics Data -- 10.5 Discussion and Conclusion -- References -- Part III Stochastic Modelling and Analysis -- 11 Stochastic Spatial Modelling of the Remyelination Process in Multiple Sclerosis Lesions -- 11.1 Introduction -- 11.2 MELA Syntax -- 11.3 MELA Semantics -- 11.4 Population Model and Dynamics -- 11.4.1 Spatial Population Model -- 11.4.2 MELA Spatial Population Model -- 11.4.3 Stochastic Dynamics and Simulation -- 11.4.4 Analysis via SSTL and Statistical Model Checking -- 11.5 MELA Remyelination Model -- 11.5.1 Background: Remyelination -- 11.5.2 MELA Remyelination Model -- 11.5.3 SSTL Properties -- 11.6 Case Study -- 11.6.1 Scenario 1: Different Probabilities of Expressing Signals -- 11.6.2 Scenario 2: Faster OPC Movement -- 11.6.3 Scenario 3: Slower OPC Movement -- 11.6.4 Failure to Repair: Not Enough OPCs or No Maturation Process? -- 11.6.5 Scenario 4: Instant Stopping Inside the Lesion -- 11.6.6 Scenario 5: Stopping in the Centre of the Lesion -- 11.7 Discussion -- 11.8 Conclusions and Future Work -- References -- 12 Approximation Techniques for Stochastic Analysis of Biological Systems -- 12.1 Introduction -- 12.2 Related Work -- 12.3 Preliminaries -- 12.4 Motivating Example -- 12.5 State-Space Approximation and Analysis -- 12.6 Proof of the Termination Condition -- 12.7 Results -- 12.7.1 Toggle Switch -- 12.7.2 Comparisons with the STAR Tool -- 12.8 Conclusion -- References -- 13 A Graphical Approach for Hybrid Modelling of Intracellular Calcium Dynamics Based on Coloured Hybrid Petri Nets -- 13.1 Introduction -- 13.2 Background -- 13.2.1 Calcium Dynamics -- 13.2.2 Coloured Hybrid Petri Nets -- 13.3 Model Construction -- 13.3.1 Dynamics of Channel Transitions -- 13.3.2 Spatial Modelling of Ca2+ Flow and Diffusion -- 13.3.3 From Stochastic to Deterministic Regime. , 13.3.4 From Deterministic to Stochastic Regime -- 13.3.5 Comparison with Other Petri Net Classes -- 13.4 Model Validation -- 13.4.1 Simulation of One Cluster with One Channel -- 13.4.2 Simulation of One Cluster with Many Channels -- 13.4.3 Simulation of Many Clusters with Many Channels -- 13.5 Simulation Procedure -- 13.6 Conclusion -- References -- 14 Methods for Personalised Delivery Rate Computation for IV Administered Anesthetic Propofol -- 14.1 Introduction -- 14.2 Prior Research Works -- 14.3 Pharmacokinetic Modelling -- 14.3.1 The State-Space Representation of PK Model -- 14.3.2 Inter- and Intra-individual Variability -- 14.3.3 Schnider Versus Eleveld Model -- 14.4 Classic Open-Loop TCI Algorithm -- 14.5 Closed-Loop Control -- 14.5.1 Feedback Loop with Bayesian Approach -- 14.5.2 Feedback Loop with Kalman Filter -- 14.6 Robustness Analysis -- 14.6.1 Computer-Aided Clinical Trials -- 14.6.2 Experimental Setup -- 14.6.3 Robustness Versus Period of Measurements -- 14.6.4 Realistic Measurement Scenario -- 14.7 Discussion -- References -- Part IV Machine Learning and Artificial Intelligence -- 15 Towards the Integration of Metabolic Network Modelling and Machine Learning for the Routine Analysis of High-Throughput Patient Data -- 15.1 Introduction -- 15.2 Reference Datasets -- 15.3 Constraint-Based Modelling -- 15.3.1 Metabolic Modelling -- 15.4 Machine Learning -- 15.4.1 Supervised Machine Learning -- 15.4.2 Unsupervised Machine Learning -- 15.5 Machine Learning and Constraint-Based Modelling -- 15.5.1 Predicting Growth Rates and Metabolite Prediction -- 15.5.2 Machine Learning and Essential Genes -- 15.5.3 Prediction of Side Effects -- 15.5.4 Prediction of Biomarkers and the Use of a Combined Approach to Analyse Patient Data -- 15.6 Discussion -- References -- 16 Opportunities and Challenges in Applying Artificial Intelligence to Bioengineering. , 16.1 Introduction.