Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Formal modeling and analysis of timed systems : 20th international conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, proceedings / / Sergiy Bogomolov, David Parker (editors)
| Formal modeling and analysis of timed systems : 20th international conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, proceedings / / Sergiy Bogomolov, David Parker (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (315 pages) |
| Disciplina | 003.3 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer simulation
Formal methods (Computer science) System analysis |
| ISBN | 3-031-15839-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts -- A Behaviour-Based Approach to Quantitative Validation of Cyber-Physical Systems -- A Personal History of Formal Modeling and Analysis of Timed Systems Before There was FORMATS -- Contents -- Invited Papers -- Algebraic Model Checking for Discrete Linear Dynamical Systems -- 1 Introduction -- 1.1 Skolem Oracles -- 1.2 Main Results -- 2 Algebraic Model Checking -- 3 Conclusion -- References -- Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next? -- 1 Introduction -- 2 Birth of Timed Automata for Verification: The Early 90's -- 2.1 Preliminaries -- 2.2 The Timed Automaton Model ch2AD90,ch2AD94 -- 3 A Symbolic Approach to the Verification of Timed Automata -- 3.1 Zones and Symbolic Forward Computation -- 3.2 Difference Bounded Matrices (DBMs) -- 3.3 Efficiency of the Forward Analysis -- 4 Extrapolation: A First Solution -- 4.1 The First Extrapolation Operator -- 4.2 Two Refinements of This Approach -- 4.3 Problems with Diagonal Clock Constraints -- 5 Simulation: An Alternative Solution -- 6 Beyond Reachability -- 6.1 Weighted Timed Automata -- 6.2 Liveness Properties -- 7 Tools -- 7.1 A Tool for Verifying Timed Automata: Uppaal -- 7.2 The Tool TChecker -- 8 What Next? -- 8.1 BDD and SAT Based Methods -- 8.2 The Local-Time Semantics and Partial-Order Reduction -- 8.3 Domain-Specific Algorithms -- 8.4 Richer Models -- References -- Monitoring Timed Properties (Revisited) -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 4 Monitoring in a Timed Setting -- 5 Time Divergence -- 6 A Symbolic Method for Monitoring -- 7 Time Uncertainty -- 8 Time Predictive Monitoring -- 9 Conclusion -- References -- Probabilistic and Timed Systems -- Bounded Delay Timed Channel Coding -- 1 Introduction -- 2 Preliminary Work -- 2.1 Timed Languages and Timed Automata.
2.2 Entropy and Capacity -- 2.3 Pseudo-Distance on Timed Languages -- 2.4 The Factor Language -- 3 Bandwidth -- 3.1 Definitions -- 3.2 Examples -- 3.3 Existence of Limits -- 4 Encodings -- 4.1 Definition -- 4.2 Necessary Condition -- 4.3 Sufficient Condition -- 5 Conclusion and Further Work -- References -- Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Canonical Sample Space -- 2.2 Markov Transition Systems -- 2.3 Weak Convergence and Prokhorov's Theorem -- 2.4 Discrete-Time Continuous-State Stochastic Systems -- 2.5 Robust Abstractions -- 3 Soundness of Robust IMC Abstractions -- 3.1 Weak Compactness of Marginal Space Mt of Probabilities -- 3.2 Weak Compactness of Probability Laws of I on Infinite Horizon -- 3.3 Soundness of IMC Abstractions -- 4 Robust Completeness of IMC Abstractions -- 5 Conclusion -- References -- Model Checking for Entanglement Swapping -- 1 Introduction -- 2 Preliminaries -- 2.1 Probabilistic Timed Automata -- 3 Modeling and Validation -- 3.1 The PTA Model -- 3.2 Validation Through Simulations -- 4 Experimental Setup -- 5 Results -- 6 Discussions and Outlook -- References -- Temporal Logic -- An STL-Based Formulation of Resilience in Cyber-Physical Systems -- 1 Introduction -- 2 Preliminaries -- 3 Specifying Resilience in STL -- 3.1 Resiliency Specification Language -- 3.2 Semantics of Resiliency Specifications -- 4 Case Study -- 4.1 UAV Package Delivery -- 4.2 Multi-agent Flocking -- 5 Related Work -- 6 Conclusion -- References -- MITL Verification Under Timing Uncertainty -- 1 Introduction -- 2 Preliminaries -- 2.1 Set Theory -- 2.2 Topology -- 3 Problem Formulation -- 3.1 Syntax and Semantics of MITL -- 3.2 Truth Sets and Interval Queues -- 4 Interval Queue Fundamentals -- 4.1 Construction Algorithm -- 4.2 Complementation Algorithm. 5 Verification Procedure -- 5.1 Operators in the Interval Queue Domain -- 5.2 Constructing Under- and Over-Approximations -- 5.3 Conservativeness -- 6 Numerical Example -- 7 Conclusion -- A Proof of Theorem 1 -- References -- Classification of Driving Behaviors Using STL Formulas: A Comparative Study -- 1 Introduction -- 2 Preliminaries -- 3 Specifying Longitudinal Driving Behavior with STL -- 4 Methods -- 5 Experiments -- 6 Discussion and Conclusions -- References -- Timed Automata and Games -- Timed Games with Bounded Window Parity Objectives -- 1 Introduction -- 2 Preliminaries -- 3 Bounded Window Objectives -- 4 Verification of Timed Automata -- 5 Solving Timed Games -- References -- Non-blind Strategies in Timed Network Congestion Games -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Network Congestion Game -- 2.2 Studied Problems -- 3 Existence and Computation of Nash Equilibria -- 3.1 Transformation into an Equivalent Finite Concurrent Game -- 3.2 Existence of Nash Equilibria -- 3.3 Computation of Nash Equilibria -- 4 Social Optimality and Prices of Anarchy and Stability -- 4.1 Constrained-Social-Welfare Problem: Asymmetric Case -- 4.2 Constrained-Social-Welfare Problem: Symmetric Case -- 4.3 Social Optimum and Prices of Anarchy and Stability -- References -- Efficient Convex Zone Merging in Parametric Timed Automata -- 1 Introduction -- 2 Preliminaries -- 3 Efficient State Merging in Parametric Timed Automata -- 3.1 Merging Algorithm -- 3.2 Heuristics for Merging -- 3.3 Preservation of Properties -- 4 Experiments -- 4.1 Dataset and Experimental Environment -- 4.2 Description of the Experiments -- 5 Conclusion -- A Results for All Heuristics on the Full Benchmark -- References -- Neural Networks -- Neural Network Repair with Reachability Analysis -- 1 Introduction -- 2 Deep Neural Network Repair -- 2.1 Provably Safe DNNs. 2.2 DNN Agent Repair for Deep Reinforcement Learning -- 2.3 Computation of Exact Unsafe Domain of ReLU DNNs -- 3 Framework for DNN Repair -- 3.1 Formulation of Loss Function for Problems 1 & -- 2 -- 3.2 Repair for Deep Reinforcement Learning -- 4 Experiments and Evaluation -- 4.1 Repair of ACAS Xu Neural Network Controllers -- 4.2 Rocket Lander Benchmark -- 5 Conclusion and Future Work -- References -- On Neural Network Equivalence Checking Using SMT Solvers -- 1 Introduction -- 2 Preliminaries: Neural Networks -- 2.1 Notation -- 2.2 Neural Networks -- 3 Strict and Approximate Equivalences for Neural Networks -- 3.1 Strict Neural Network Equivalence -- 3.2 Approximate Neural Network Equivalences Based on Lp Norms -- 3.3 Approximate Neural Network Equivalences Based on Order of Outputs -- 3.4 Hybrid Lp-argsort Equivalences -- 3.5 The Neural Network Equivalence Checking Problem -- 3.6 Discussion of Application Domains for the Above Equivalence Relations -- 4 Neural Network Equivalence Checking Using SMT Solvers -- 4.1 Encoding Neural Networks as SMT Formulas -- 4.2 Encoding of the Equivalence Relation -- 4.3 Optimizing the Encoding -- 5 Experimental Results -- 5.1 Sanity Checks -- 5.2 Equivalence Checking -- 6 Related Work -- 7 Conclusions -- References -- Reachability Analysis of a General Class of Neural Ordinary Differential Equations -- 1 Introduction -- 2 Background and Problem Formulation -- 2.1 General Neural ODE -- 2.2 NODE: Applications -- 2.3 Reachability Analysis -- 2.4 Reachability Methods -- 3 Evaluation -- 3.1 Method and Tool Comparison -- 3.2 Case Study: Adaptive Cruise Control (ACC) -- 3.3 Classification NODEs -- 4 Related Work -- 5 Conclusion and Future Work -- References -- Reinforcement Learning -- Robust Event-Driven Interactions in Cooperative Multi-agent Learning -- 1 Introduction -- 1.1 Main Contribution -- 2 Preliminaries. 2.1 Notation -- 2.2 MDPs and Multi-agent MDPs -- 2.3 Value Functions and Q-Learning in c-MMDPs -- 3 Information Sharing Between Collaborative Agents: Problem Formulation -- 4 Efficient Communication Strategies -- 4.1 Event-Driven Interactions -- 5 Robustness Surrogate and Its Computation -- 5.1 Learning the Robustness Surrogate with the Scenario Approach -- 6 Experiments -- 6.1 Benchmark: Collaborative Particle-Tag -- 6.2 Computation of Robustness Surrogates -- 6.3 Results -- 7 Discussion -- References -- Learning that Grid-Convenience Does Not Hurt Resilience in the Presence of Uncertainty -- 1 Introduction -- 2 Case Study -- 3 Methodology -- 4 Results -- 5 Reproducibility and Conclusions -- References -- Author Index. |
| Record Nr. | UNINA-9910590070203321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal modeling and analysis of timed systems : 20th international conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, proceedings / / Sergiy Bogomolov, David Parker (editors)
| Formal modeling and analysis of timed systems : 20th international conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, proceedings / / Sergiy Bogomolov, David Parker (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (315 pages) |
| Disciplina | 003.3 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer simulation
Formal methods (Computer science) System analysis |
| ISBN | 3-031-15839-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts -- A Behaviour-Based Approach to Quantitative Validation of Cyber-Physical Systems -- A Personal History of Formal Modeling and Analysis of Timed Systems Before There was FORMATS -- Contents -- Invited Papers -- Algebraic Model Checking for Discrete Linear Dynamical Systems -- 1 Introduction -- 1.1 Skolem Oracles -- 1.2 Main Results -- 2 Algebraic Model Checking -- 3 Conclusion -- References -- Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next? -- 1 Introduction -- 2 Birth of Timed Automata for Verification: The Early 90's -- 2.1 Preliminaries -- 2.2 The Timed Automaton Model ch2AD90,ch2AD94 -- 3 A Symbolic Approach to the Verification of Timed Automata -- 3.1 Zones and Symbolic Forward Computation -- 3.2 Difference Bounded Matrices (DBMs) -- 3.3 Efficiency of the Forward Analysis -- 4 Extrapolation: A First Solution -- 4.1 The First Extrapolation Operator -- 4.2 Two Refinements of This Approach -- 4.3 Problems with Diagonal Clock Constraints -- 5 Simulation: An Alternative Solution -- 6 Beyond Reachability -- 6.1 Weighted Timed Automata -- 6.2 Liveness Properties -- 7 Tools -- 7.1 A Tool for Verifying Timed Automata: Uppaal -- 7.2 The Tool TChecker -- 8 What Next? -- 8.1 BDD and SAT Based Methods -- 8.2 The Local-Time Semantics and Partial-Order Reduction -- 8.3 Domain-Specific Algorithms -- 8.4 Richer Models -- References -- Monitoring Timed Properties (Revisited) -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 4 Monitoring in a Timed Setting -- 5 Time Divergence -- 6 A Symbolic Method for Monitoring -- 7 Time Uncertainty -- 8 Time Predictive Monitoring -- 9 Conclusion -- References -- Probabilistic and Timed Systems -- Bounded Delay Timed Channel Coding -- 1 Introduction -- 2 Preliminary Work -- 2.1 Timed Languages and Timed Automata.
2.2 Entropy and Capacity -- 2.3 Pseudo-Distance on Timed Languages -- 2.4 The Factor Language -- 3 Bandwidth -- 3.1 Definitions -- 3.2 Examples -- 3.3 Existence of Limits -- 4 Encodings -- 4.1 Definition -- 4.2 Necessary Condition -- 4.3 Sufficient Condition -- 5 Conclusion and Further Work -- References -- Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Canonical Sample Space -- 2.2 Markov Transition Systems -- 2.3 Weak Convergence and Prokhorov's Theorem -- 2.4 Discrete-Time Continuous-State Stochastic Systems -- 2.5 Robust Abstractions -- 3 Soundness of Robust IMC Abstractions -- 3.1 Weak Compactness of Marginal Space Mt of Probabilities -- 3.2 Weak Compactness of Probability Laws of I on Infinite Horizon -- 3.3 Soundness of IMC Abstractions -- 4 Robust Completeness of IMC Abstractions -- 5 Conclusion -- References -- Model Checking for Entanglement Swapping -- 1 Introduction -- 2 Preliminaries -- 2.1 Probabilistic Timed Automata -- 3 Modeling and Validation -- 3.1 The PTA Model -- 3.2 Validation Through Simulations -- 4 Experimental Setup -- 5 Results -- 6 Discussions and Outlook -- References -- Temporal Logic -- An STL-Based Formulation of Resilience in Cyber-Physical Systems -- 1 Introduction -- 2 Preliminaries -- 3 Specifying Resilience in STL -- 3.1 Resiliency Specification Language -- 3.2 Semantics of Resiliency Specifications -- 4 Case Study -- 4.1 UAV Package Delivery -- 4.2 Multi-agent Flocking -- 5 Related Work -- 6 Conclusion -- References -- MITL Verification Under Timing Uncertainty -- 1 Introduction -- 2 Preliminaries -- 2.1 Set Theory -- 2.2 Topology -- 3 Problem Formulation -- 3.1 Syntax and Semantics of MITL -- 3.2 Truth Sets and Interval Queues -- 4 Interval Queue Fundamentals -- 4.1 Construction Algorithm -- 4.2 Complementation Algorithm. 5 Verification Procedure -- 5.1 Operators in the Interval Queue Domain -- 5.2 Constructing Under- and Over-Approximations -- 5.3 Conservativeness -- 6 Numerical Example -- 7 Conclusion -- A Proof of Theorem 1 -- References -- Classification of Driving Behaviors Using STL Formulas: A Comparative Study -- 1 Introduction -- 2 Preliminaries -- 3 Specifying Longitudinal Driving Behavior with STL -- 4 Methods -- 5 Experiments -- 6 Discussion and Conclusions -- References -- Timed Automata and Games -- Timed Games with Bounded Window Parity Objectives -- 1 Introduction -- 2 Preliminaries -- 3 Bounded Window Objectives -- 4 Verification of Timed Automata -- 5 Solving Timed Games -- References -- Non-blind Strategies in Timed Network Congestion Games -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Network Congestion Game -- 2.2 Studied Problems -- 3 Existence and Computation of Nash Equilibria -- 3.1 Transformation into an Equivalent Finite Concurrent Game -- 3.2 Existence of Nash Equilibria -- 3.3 Computation of Nash Equilibria -- 4 Social Optimality and Prices of Anarchy and Stability -- 4.1 Constrained-Social-Welfare Problem: Asymmetric Case -- 4.2 Constrained-Social-Welfare Problem: Symmetric Case -- 4.3 Social Optimum and Prices of Anarchy and Stability -- References -- Efficient Convex Zone Merging in Parametric Timed Automata -- 1 Introduction -- 2 Preliminaries -- 3 Efficient State Merging in Parametric Timed Automata -- 3.1 Merging Algorithm -- 3.2 Heuristics for Merging -- 3.3 Preservation of Properties -- 4 Experiments -- 4.1 Dataset and Experimental Environment -- 4.2 Description of the Experiments -- 5 Conclusion -- A Results for All Heuristics on the Full Benchmark -- References -- Neural Networks -- Neural Network Repair with Reachability Analysis -- 1 Introduction -- 2 Deep Neural Network Repair -- 2.1 Provably Safe DNNs. 2.2 DNN Agent Repair for Deep Reinforcement Learning -- 2.3 Computation of Exact Unsafe Domain of ReLU DNNs -- 3 Framework for DNN Repair -- 3.1 Formulation of Loss Function for Problems 1 & -- 2 -- 3.2 Repair for Deep Reinforcement Learning -- 4 Experiments and Evaluation -- 4.1 Repair of ACAS Xu Neural Network Controllers -- 4.2 Rocket Lander Benchmark -- 5 Conclusion and Future Work -- References -- On Neural Network Equivalence Checking Using SMT Solvers -- 1 Introduction -- 2 Preliminaries: Neural Networks -- 2.1 Notation -- 2.2 Neural Networks -- 3 Strict and Approximate Equivalences for Neural Networks -- 3.1 Strict Neural Network Equivalence -- 3.2 Approximate Neural Network Equivalences Based on Lp Norms -- 3.3 Approximate Neural Network Equivalences Based on Order of Outputs -- 3.4 Hybrid Lp-argsort Equivalences -- 3.5 The Neural Network Equivalence Checking Problem -- 3.6 Discussion of Application Domains for the Above Equivalence Relations -- 4 Neural Network Equivalence Checking Using SMT Solvers -- 4.1 Encoding Neural Networks as SMT Formulas -- 4.2 Encoding of the Equivalence Relation -- 4.3 Optimizing the Encoding -- 5 Experimental Results -- 5.1 Sanity Checks -- 5.2 Equivalence Checking -- 6 Related Work -- 7 Conclusions -- References -- Reachability Analysis of a General Class of Neural Ordinary Differential Equations -- 1 Introduction -- 2 Background and Problem Formulation -- 2.1 General Neural ODE -- 2.2 NODE: Applications -- 2.3 Reachability Analysis -- 2.4 Reachability Methods -- 3 Evaluation -- 3.1 Method and Tool Comparison -- 3.2 Case Study: Adaptive Cruise Control (ACC) -- 3.3 Classification NODEs -- 4 Related Work -- 5 Conclusion and Future Work -- References -- Reinforcement Learning -- Robust Event-Driven Interactions in Cooperative Multi-agent Learning -- 1 Introduction -- 1.1 Main Contribution -- 2 Preliminaries. 2.1 Notation -- 2.2 MDPs and Multi-agent MDPs -- 2.3 Value Functions and Q-Learning in c-MMDPs -- 3 Information Sharing Between Collaborative Agents: Problem Formulation -- 4 Efficient Communication Strategies -- 4.1 Event-Driven Interactions -- 5 Robustness Surrogate and Its Computation -- 5.1 Learning the Robustness Surrogate with the Scenario Approach -- 6 Experiments -- 6.1 Benchmark: Collaborative Particle-Tag -- 6.2 Computation of Robustness Surrogates -- 6.3 Results -- 7 Discussion -- References -- Learning that Grid-Convenience Does Not Hurt Resilience in the Presence of Uncertainty -- 1 Introduction -- 2 Case Study -- 3 Methodology -- 4 Results -- 5 Reproducibility and Conclusions -- References -- Author Index. |
| Record Nr. | UNISA-996485665403316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Management of Knee Osteoarthritis in the Younger, Active Patient : An Evidence-Based Practical Guide for Clinicians / / edited by David Parker
| Management of Knee Osteoarthritis in the Younger, Active Patient : An Evidence-Based Practical Guide for Clinicians / / edited by David Parker |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (165 p.) |
| Disciplina | 610 |
| Soggetto topico |
Orthopedics
Sports medicine Surgical Orthopedics Conservative Orthopedics Sports Medicine |
| ISBN | 3-662-48530-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction, and Nonoperative Management: Osteoarthritis – Definition, Aetiology & Natural History -- Nonsurgical Management of Osteoarthritis. Surgical Management: Meniscus Surgery -- Arthroscopic Debridement in the Presence of Osteoarthritis -- Cartilage Preservation & Restoration -- Osteotomy around the knee -- Unicompartmental Knee Arthroplasty -- Total Knee Arthroplasty -- New and Evolving Surgical Techniques -- Conclusions and Future Directions. |
| Record Nr. | UNINA-9910254559103321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model Checking Software [[electronic resource] ] : 19th International SPIN Workshop, Oxford, UK, July 23-24, 2012. Proceedings / / edited by Alastair Donaldson, David Parker
| Model Checking Software [[electronic resource] ] : 19th International SPIN Workshop, Oxford, UK, July 23-24, 2012. Proceedings / / edited by Alastair Donaldson, David Parker |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (X, 261 p. 85 illus.) |
| Disciplina | 005.3028/7 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming |
| ISBN | 3-642-31759-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996465491603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Neuronal Co-transmission
| Neuronal Co-transmission |
| Autore | Apergis-Schoute John |
| Pubbl/distr/stampa | Frontiers Media SA, 2019 |
| Descrizione fisica | 1 online resource (184 p.) |
| Soggetto topico |
Neurosciences
Science: general issues |
| Soggetto non controllato |
Co-existence
co-localization co-release co-transmission monoamines Neuropeptides Neurotransmitter complexity Neurotransmitter segregation |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910557641403321 |
Apergis-Schoute John
|
||
| Frontiers Media SA, 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Positron Emission Particle Tracking : A Comprehensive Guide
| Positron Emission Particle Tracking : A Comprehensive Guide |
| Autore | Windows-Yule Kit |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Bristol : , : Institute of Physics Publishing, , 2022 |
| Descrizione fisica | 1 online resource (699 pages) |
| Altri autori (Persone) |
ParkerDavid
MangerSamuel NicuşanAndrei L HeraldMatthew T |
| Collana | IOP Ebooks Series |
| Soggetto topico |
Positron beams
Tracers (Chemistry) |
| ISBN |
9780750344135
075034413X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Acknowledgement -- Author biographies -- Kit Windows-Yule -- Leonard Nicuşan -- Matthew T Herald -- Samuel Manger -- David Parker -- Chapter 0 Using the book -- 0.1 The 'User' -- 0.2 The 'Researcher' -- 0.3 The 'Developer' -- 0.4 The 'Expert' -- Chapter 1 Imaging particulate and multiphase systems -- 1.1 Particulate and multiphase systems: why do they matter? -- 1.2 The importance of imaging -- 1.3 Particle and flow imaging: an overview -- References -- Chapter 2 The fundamentals of PEPT -- 2.1 Positron emission… -- 2.2 …particle tracking -- 2.2.1 Interactive example: PEPT-an idealised case -- PEPT: an idealised case -- Monte Carlo line of response generation -- Triangulate tracer's location -- Spatial error versus number of LoRs used -- 2.3 A more realistic picture -- 2.3.1 Issue 1: false coincidences -- 2.3.2 Issue 2: positron flight -- 2.3.3 Issue 3: imperfect detectors -- 2.3.4 Issue 4: finite detection rate -- 2.3.5 The real picture -- 2.3.6 Interactive example: sources of error in PEPT -- Sources of error in PEPT -- Monte Carlo line of response generation -- Adding noise: scattered events and spread -- Triangulate tracer's location -- Spatial error versus noise ratio -- 2.4 Not just particle tracking -- References -- Chapter 3 A history of PEPT -- 3.1 Adding the 'P': from PET to PEPT (origins to 1989) -- 3.2 MWPC PEPT (1989-1999) -- 3.3 Out with the old, in with the new (1999-2002) -- 3.4 Positron cameras of all shapes and sizes (2002-present) -- 3.5 PEPT elsewhere -- 3.6 The future-SuperPEPT, MicroPEPT and beyond -- References -- Chapter 4 Comparison with other techniques -- 4.1 Quasi-two-dimensional techniques -- 4.1.1 Particle tracking velocimetry (PTV) -- 4.1.2 Particle imaging velocimetry (PIV) -- 4.1.3 Photoelastic imaging -- 4.1.4 X-ray radiography -- 4.2 Tomographic techniques -- 4.2.1 X-ray computed tomography.
4.2.2 Single-photon emission computed tomography (SPECT) -- 4.2.3 Positron emission tomography (PET) -- 4.2.4 Electrical capacitance tomography (ECT) -- 4.2.5 Magnetic resonance imaging (MRI) -- 4.2.6 Refractive index matched scanning (RIMS) -- 4.3 Three-dimensional particle-tracking techniques -- 4.3.1 Radioactive particle tracking (RPT) -- 4.3.2 Magnetic particle tracking (MPT) -- 4.4 Non-imaging techniques -- Angle of repose (AOR) tests -- Tapped density tests-the Carr index and Hausner ratio -- Flow through an orifice -- Shear testing -- Powder rheometry -- 4.5 Numerical simulation -- 4.5.1 The discrete element method (DEM) -- A simple discrete element method simulation -- Define system of differential equations -- Numerically solving the ODE: Euler method -- Numerically solving the ODE: adaptive integration schemes -- 4.5.2 Computational fluid dynamics (CFD) -- 4.5.3 The Monte Carlo method -- A simple Monte Carlo simulation -- How many random samples? -- 4.6 Other techniques -- References -- Chapter 5 Tracers and detectors -- 5.1 Creating tracers -- 5.1.1 Introduction-the ideal tracer -- 5.1.2 Positron-emitting nuclides and direct activation -- 5.1.3 Indirect activation -- 5.1.4 Handling and coating -- 5.2 Detector systems -- 5.2.1 Introduction -- 5.2.2 Scintillation detectors -- 5.2.3 PEPT system geometries -- 5.2.4 Examples of PEPT systems -- 5.2.5 Future developments -- 5.3 Modelling PEPT systems -- 5.3.1 How it works -- 5.3.2 Existing GATE models -- 5.3.3 Modelling a PEPT detector -- 5.3.4 Defining a PEPT tracer -- 5.3.5 Recreating an experiment -- 5.3.6 Studying a PEPT system using GATE -- References -- Chapter 6 Pre-processing: PEPT data and algorithms -- 6.1 Understanding PEPT data -- 6.1.1 Interactive example: PEPT data format -- PEPT Data Format -- Initialise raw line of response data -- Visualising a sample of LoRs. Temporal resolution? -- 6.2 Available algorithms -- 6.2.1 The Birmingham algorithm -- 6.2.2 Interactive example: the Birmingham algorithm -- Interactive PEPT analysis example using the Birmingham method [1] -- This Jupyter Notebook -- Initialise raw line of response data -- Find minimum distance point -- Remove the farthest lines of response -- Iteratively remove the farthest LoRs and recompute MDP -- Complete Birmingham Method code -- High-performance Birmingham Method implementation -- 6.2.3 The line-density method -- 6.2.4 Interactive example: the line-density method -- Interactive PEPT analysis example using the line density algorithm [4] -- This Jupyter Notebook -- Initialise raw line of response data -- Voxelise the lines of response -- Fit 1D Gaussians around the peak -- Complete line density method code -- 6.2.5 The G-means clustering algorithm -- 6.2.6 Interactive example: the G-means algorithm -- Interactive PEPT analysis example using the clustering (G-means) algorithm [6] -- This Jupyter Notebook -- Initialise raw line of response data -- Voxelise the lines of response -- High pass filter -- Cluster voxels with G-means -- Complete clustering (G-means) algorithm code -- Multiple particle tracking -- 6.2.7 Feature-point identification (FPI) -- 6.2.8 Interactive example: FPI -- Interactive PEPT analysis example using the feature point identification algorithm [17] -- This Jupyter Notebook -- Initialise raw line of response data -- Voxelise the lines of response -- Subtract convolved matrix and blur -- Extract voxel peaks -- Complete FPI algorithm code -- Multiple particle tracking -- High-performance FPI algorithm implementation -- 6.2.9 Spatiotemporal B-spline reconstruction (SBSR) -- 6.2.10 Voronoi tesselation method -- 6.2.11 Interactive example: Voronoi tesselation. Interactive PEPT analysis example using the Voronoi tesselation method [30] -- This Jupyter Notebook -- Initialise raw line of response data -- Discretise the lines of response -- Voronoi tesselation -- Gather points under consideration (PUCs) -- Local filtering based on the local outlier factor -- Global filtering -- Clustering the remaining PUCs -- Extract final tracer locations -- Complete Voronoi tesselation algorithm code -- 6.2.12 The triangulation method -- 6.2.13 Interactive example: triangulation method -- Interactive PEPT analysis example using the triangulation method [37] -- This Jupyter Notebook -- Initialise raw line of response data -- Calculate the LoR distance matrix -- Cluster LoRs closer than the tracer radius -- Find centroids of clustered LoRs' cutpoints -- Complete triangulation method code -- 6.2.14 PEPT using machine learning (PEPT-ML) -- 6.2.15 Interactive example: PEPT-ML -- Interactive PEPT analysis example using the PEPT-ML algorithm [38] -- This Jupyter Notebook -- Initialise raw line of response data -- Find cutpoints -- Cluster cutpoints with HDBSCAN -- Compute cluster centres -- Complete PEPT-ML algorithm code -- Second pass of clustering -- Multiple particle tracking -- High-performance PEPT-ML algorithm implementation -- 6.2.16 PEPT using expectation-maximisation (PEPT-EM) -- 6.2.17 Interactive example: PEPT-EM -- Interactive PEPT analysis examples using PEPT-EM [44] -- This Jupyter Notebook -- Initialise Raw Line of Response Data -- Calculate MDP and assign a weight to each LoR -- Recalculate MDP with previous weights -- Complete PEPT-EM algorithm code -- 6.2.18 The K-medoids method -- 6.2.19 Interactive example: K-medoids method -- Interactive PEPT analysis example using the K-medoids method [45] -- This Jupyter Notebook -- Initialise raw line of response data -- Find cutpoints. Filter cutpoints with far nearest neighbors -- Cluster filtered cutpoints using K-medoids -- Compute clusters' centroids -- Complete K-medoids method mode -- Multiple particle pracking -- 6.2.20 The multiple location-allocation algorithm (MLAA) -- 6.2.21 Interactive example: the multiple location-allocation algorithm (MLAA) -- Interactive PEPT analysis example using the multiple location-allocation algorithm (MLAA) [49] -- This Jupyter Notebook -- Initialise raw line of response data -- Voxelise the lines of response -- Voxel global thresholding -- The location-allocation algorithm -- Complete multiple location-allocation algorithm code -- Multiple particle tracking -- 6.3 From finding tracers to tracking trajectories -- 6.3.1 Interactive example: the effects of sample size and overlap -- Effect of sample size and overlap -- Prelude -- Initialise raw line of response data -- Effect of sample size -- Effect of overlap -- 6.3.2 Trajectory extraction -- 6.3.3 Interactive example: filtering trajectories -- Filtering trajectories -- Initialising lines of response -- Filtering based on spatial error -- Filtering based on nearest neighbours -- Filtering using the PEPT Library -- 6.3.4 Interactive example: separating trajectories -- Separating trajectories -- Initialising lines of response -- PTV-based trajectory separation -- Clustering-based trajectory separation -- 6.4 Horses for courses: comparing algorithm capability for differing tasks -- References -- Chapter 7 Post-processing: extracting physical information from PEPT data -- 7.1 Particle trajectories -- 7.1.1 Single-particle trajectories and their interpretation -- 7.1.2 Interactive example: plotting single particle trajectories -- Tutorial: Using PEPT data to plot single particle trajectories -- Setting up -- Importing data -- Plotting data -- Using the pept library. 7.1.3 Interactive example: multiple-particle data. |
| Record Nr. | UNINA-9911009379403321 |
|
Windows-Yule Kit
|
||
| Bristol : , : Institute of Physics Publishing, , 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Quantitative Evaluation of Systems [[electronic resource] ] : 16th International Conference, QEST 2019, Glasgow, UK, September 10–12, 2019, Proceedings / / edited by David Parker, Verena Wolf
| Quantitative Evaluation of Systems [[electronic resource] ] : 16th International Conference, QEST 2019, Glasgow, UK, September 10–12, 2019, Proceedings / / edited by David Parker, Verena Wolf |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XI, 361 p. 595 illus., 55 illus. in color.) |
| Disciplina | 004.24 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Artificial intelligence Computer science—Mathematics Mathematical statistics Machine theory Algorithms Computer Science Logic and Foundations of Programming Software Engineering Artificial Intelligence Probability and Statistics in Computer Science Formal Languages and Automata Theory |
| ISBN | 3-030-30281-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Probabilistic Verification -- Learning and Verification -- Hybrid Systems -- Security -- Probabilistic Modelling and Abstraction -- Applications and Tools. |
| Record Nr. | UNISA-996466285503316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Quantitative Evaluation of Systems : 16th International Conference, QEST 2019, Glasgow, UK, September 10–12, 2019, Proceedings / / edited by David Parker, Verena Wolf
| Quantitative Evaluation of Systems : 16th International Conference, QEST 2019, Glasgow, UK, September 10–12, 2019, Proceedings / / edited by David Parker, Verena Wolf |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XI, 361 p. 595 illus., 55 illus. in color.) |
| Disciplina |
004.24
004.25 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Artificial intelligence Computer science—Mathematics Mathematical statistics Machine theory Algorithms Computer Science Logic and Foundations of Programming Software Engineering Artificial Intelligence Probability and Statistics in Computer Science Formal Languages and Automata Theory |
| ISBN | 3-030-30281-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Probabilistic Verification -- Learning and Verification -- Hybrid Systems -- Security -- Probabilistic Modelling and Abstraction -- Applications and Tools. |
| Record Nr. | UNINA-9910349299203321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part II / / edited by Armin Biere, David Parker
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part II / / edited by Armin Biere, David Parker |
| Autore | Biere Armin |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (XXIII, 425 p. 1 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computers, Special purpose Computer systems Microprogramming Computer science—Mathematics Software Engineering Special Purpose and Application-Based Systems Computer System Implementation Control Structures and Microprogramming Mathematics of Computing |
| ISBN | 3-030-45237-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Bisimulation -- Verification and Efficiency -- Logic and Proof -- Tools and Case Studies -- Games and Automata -- SV-COMP 2020. |
| Record Nr. | UNISA-996418216303316 |
|
Biere Armin
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I / / edited by Armin Biere, David Parker
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I / / edited by Armin Biere, David Parker |
| Autore | Biere Armin |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (XXIII, 501 p. 1 illus.) |
| Disciplina | 004.0151 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Computers, Special purpose Computer systems Microprogramming Computer science—Mathematics Theory of Computation Special Purpose and Application-Based Systems Computer System Implementation Control Structures and Microprogramming Mathematics of Computing |
| ISBN | 3-030-45190-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Program Verification -- SAT and SMT -- Timed and Dynamical Systems -- Verifying Concurrent Systems -- Probabilistic Systems -- Model Checking and Reachability -- Timed and Probabilistic Systems. |
| Record Nr. | UNISA-996418215003316 |
|
Biere Armin
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
