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 : 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010 : proceedings / / Krishnendu Chatterjee, Thomas A. Henzinger (eds.)
| Formal modeling and analysis of timed systems : 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010 : proceedings / / Krishnendu Chatterjee, Thomas A. Henzinger (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | New York, : Springer, 2010 |
| Descrizione fisica | 1 online resource (X, 257 p. 55 illus.) |
| Disciplina | 004.01/51 |
| Altri autori (Persone) |
ChatterjeeKrishnendu
HenzingerT. A (Thomas A.) |
| Collana | Lecture notes in computer science, 0302-9743 |
| Soggetto topico |
Computer simulation
Temporal automata Formal methods (Computer science) Machine theory |
| ISBN |
1-280-38846-3
9786613566386 3-642-15297-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Interdisciplinary Foundations for Open Cyber-Physical Systems -- Safraless Procedures for Timed Specifications -- Property-Based Monitoring of Analog and Mixed-Signal Systems -- A Framework for Verification of Software with Time and Probabilities -- Synchrony and Time in Fault-Tolerant Distributed Algorithms -- Reconciling Urgency and Variable Abstraction in a Hybrid Compositional Setting -- Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games -- Natural Domain SMT: A Preliminary Assessment -- Robust Satisfaction of Temporal Logic over Real-Valued Signals -- Combining Symbolic Representations for Solving Timed Games -- Expected Reachability-Time Games -- Diagnosis Using Unfoldings of Parametric Time Petri Nets -- From Mtl to Deterministic Timed Automata -- Unambiguity in Timed Regular Languages: Automata and Logics -- A Process Algebraic Framework for Modeling Resource Demand and Supply -- Memory Event Clocks -- Simulation and Bisimulation for Probabilistic Timed Automata -- Layered Composition for Timed Automata -- A Conformance Testing Relation for Symbolic Timed Automata. |
| Record Nr. | UNINA-9910483179603321 |
| New York, : Springer, 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal modeling and analysis of timed systems : 7th international conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009 : proceedings / / Joel Ouaknine, Frits W. Vaandrager (eds.)
| Formal modeling and analysis of timed systems : 7th international conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009 : proceedings / / Joel Ouaknine, Frits W. Vaandrager (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2009 |
| Descrizione fisica | 1 online resource (X, 291 p.) |
| Disciplina | 004n/a |
| Altri autori (Persone) |
OuaknineJoel
VaandragerFrits |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer simulation
Formal methods (Computer science) Temporal automata |
| ISBN | 3-642-04368-2 |
| Classificazione |
DAT 260f
DAT 510f DAT 550f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tapas: Theory Combinations and Practical Applications -- Max-plus Algebraic Tools for Discrete Event Systems, Static Analysis, and Zero-Sum Games -- Approximations of Discrete, Continuous, and Hybrid Systems -- Volume and Entropy of Regular Timed Languages: Analytic Approach -- Synthesis of Non-Interferent Timed Systems -- Critical Paths in the Partial Order Unfolding of a Stochastic Petri Net -- Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis -- Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation -- Model Checking Logic WCTL with Multi Constrained Modalities on One Clock Priced Timed Automata -- Safe Runtime Verification of Real-Time Properties -- Removing All Silent Transitions from Timed Automata -- Realizability of Real-Time Logics -- Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata -- Analyzing Real-Time Event-Driven Programs -- A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata -- Compositional Abstraction for Stochastic Systems -- Stochastic Games for Verification of Probabilistic Timed Automata -- Checking Timed Büchi Automata Emptiness Using LU-Abstractions -- On the Supports of Recognizable Timed Series -- Machine-Assisted Parameter Synthesis of the Biphase Mark Protocol Using Event Order Abstraction -- Exploiting Timed Automata for Conformance Testing of Power Measurements. |
| Altri titoli varianti | FORMATS 2009 |
| Record Nr. | UNINA-9910484859603321 |
| Berlin ; ; New York, : Springer, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal modeling and analysis of timed systems : 4th international conference, FORMATS 2006, Paris, France, September 25-27, 2006 : proceedings / / Eugene Asarin, Patricia Bouyer (eds.)
| Formal modeling and analysis of timed systems : 4th international conference, FORMATS 2006, Paris, France, September 25-27, 2006 : proceedings / / Eugene Asarin, Patricia Bouyer (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2006 |
| Descrizione fisica | 1 online resource (XII, 372 p.) |
| Disciplina | 004.01/51 |
| Altri autori (Persone) |
AsarinE. A (Evgenii Aleksandrovich)
BouyerPatricia <1976-> |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico |
Computer simulation
Temporal automata Formal methods (Computer science) |
| ISBN | 3-540-45031-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Timed Alternating-Time Temporal Logic -- Concurrent Semantics Without the Notions of State or State Transitions -- Decidability and Expressive Power of Real Time Logics -- Contributed Papers -- Extended Directed Search for Probabilistic Timed Reachability -- Intersection of Regular Signal-Event (Timed) Languages -- Refinements and Abstractions of Signal-Event (Timed) Languages -- Bridging the Gap Between Timed Automata and Bounded Time Petri Nets -- Matching Scenarios with Timing Constraints -- Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata -- Model Checking Timed Automata with Priorities Using DBM Subtraction -- Symbolic Robustness Analysis of Timed Automata -- Coping with the Parallelism of BitTorrent: Conversion of PEPA to ODEs in Dealing with State Space Explosion -- Temporal Logic Verification Using Simulation -- Undecidable Problems About Timed Automata -- On Timed Simulation Relations for Hybrid Systems and Compositionality -- Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling -- On the Computational Power of Timed Differentiable Petri Nets -- Model-Checking Timed ATL for Durational Concurrent Game Structures -- A Dose of Timed Logic, in Guarded Measure -- From MITL to Timed Automata -- Adding Invariants to Event Zone Automata -- Static Analysis for State-Space Reduction of Polygonal Hybrid Systems -- On the Expressiveness of MTL with Past Operators -- Simulator for Real-Time Abstract State Machines -- A Characterization of Meaningful Schedulers for Continuous-Time Markov Decision Processes. |
| Altri titoli varianti | FORMATS 2006 |
| Record Nr. | UNINA-9910768186503321 |
| Berlin ; ; New York, : Springer, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal modeling and analysis of timed systems : third international conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005 : proceedings / / Paul Pettersson, Wang Yi (eds.)
| Formal modeling and analysis of timed systems : third international conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005 : proceedings / / Paul Pettersson, Wang Yi (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2005 |
| Descrizione fisica | 1 online resource (IX, 305 p.) |
| Disciplina | 003/.3 |
| Altri autori (Persone) |
PetterssonPaul
YiWang |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer simulation
Temporal automata Formal methods (Computer science) Robots |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk -- Modular Performance Analysis of Distributed Embedded Systems -- Logic and Specification -- Real Time Temporal Logic: Past, Present, Future -- Translating Timed I/O Automata Specifications for Theorem Proving in PVS -- Specification and Refinement of Soft Real-Time Requirements Using Sequence Diagrams -- Times Games and Synthesis -- On Optimal Timed Strategies -- Average Reward Timed Games -- Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness -- Invited Talk -- Verification of Parameterized Timed Systems -- Model Checking -- Model Checking the Time to Reach Agreement -- Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems -- A New Verification Procedure for Partially Clairvoyant Scheduling -- Invited Talk -- Timing Analysis and Simulation Tools for Real-Time Control -- Hybrid Systems -- Automatic Rectangular Refinement of Affine Hybrid Systems -- Reachability Problems on Extended O-Minimal Hybrid Automata -- Counterexamples for Timed Probabilistic Reachability -- Petri Nets -- Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets -- Comparison of the Expressiveness of Timed Automata and Time Petri Nets -- Semantics -- Quantifying Similarities Between Timed Systems -- Performance of Pipelined Asynchronous Systems -- Is Timed Branching Bisimilarity an Equivalence Indeed? -- Semantics and Modelling -- Implementation of Timed Automata: An Issue of Semantics or Modeling? -- Timed Abstract Non-interference. |
| Record Nr. | UNINA-9910483853003321 |
| Berlin ; ; New York, : Springer, c2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
An introduction to practical formal methods using temporal logic [[electronic resource] /] / Michael Fisher
| An introduction to practical formal methods using temporal logic [[electronic resource] /] / Michael Fisher |
| Autore | Fisher Michael <1962-> |
| Edizione | [1st edition] |
| Pubbl/distr/stampa | Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 |
| Descrizione fisica | 1 online resource (710 p.) |
| Disciplina |
005.131
511.3 |
| Soggetto topico |
Temporal automata
Logic, Symbolic and mathematical |
| ISBN |
1-119-99146-3
1-283-40534-2 9786613405340 1-119-99148-X 1-119-99147-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Cover; Title Page; Copyright; Preface; Chapter 1: Introduction; 1.1 Aims of the Book; 1.2 Why Temporal Logic?; 1.3 What is Temporal Logic?; 1.4 Structure of the Book; Chapter 2: Temporal Logic; 2.1 Intuition; 2.2 Syntactic Aspects; 2.3 Semantics; 2.4 Reactive System Properties; 2.5 What is Temporal Logic?; 2.6 Normal Form; 2.7 Büchi Automata and Temporal Logic; 2.8 Advanced Topics; 2.9 Final Exercises; Chapter 3: Specification; 3.1 Describing Simple Behaviours; 3.2 A Semantics of Imperative Programs; 3.3 Linking Specifications; 3.4 Advanced Topics; 3.5 Final Exercises; 3.6 Where to Next?
Chapter 4: Deduction4.1 Temporal Proof; 4.2 Clausal Temporal Resolution; 4.3 The TSPASS System; 4.4 Advanced topics; 4.5 Final Exercises; Chapter 5: Model Checking; 5.1 Algorithmic Verification; 5.2 Automata-Theoretic Model Checking; 5.3 The Spin System; 5.4 Advanced Topics; 5.5 Final Exercises; Chapter 6: Execution; 6.1 From Specifications to Programs; 6.2 METATEM: Executing Temporal Formulae; 6.3 The Concurrent MetateM system; 6.4 Advanced Topics; Chapter 7: Selected Applications; 7.1 Model Checking Programs; 7.2 Security Protocol Analysis; 7.3 Recognizing Temporal Patterns 7.4 Parameterized Systems7.5 Reasoning with Intervals; 7.6 Planning; Chapter 8: Summary; Appendix A: Review of Classical Logic; A.1 Introduction; A.2 Propositional Logic; A.3 Normal Forms; A.4 Propositional Resolution; A.5 Horn Clauses; A.6 First-Order Logic; Appendix B: Solutions to Exercises; B.1 Solutions: Chapter 2; Solutions: Chapter 3; Solutions: Chapter 4; Solutions: Chapter 5; Solutions: Chapter 6; Solutions: Appendix A; References; Index |
| Record Nr. | UNINA-9910130871603321 |
Fisher Michael <1962->
|
||
| Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
An introduction to practical formal methods using temporal logic / / Michael Fisher
| An introduction to practical formal methods using temporal logic / / Michael Fisher |
| Autore | Fisher Michael <1962-> |
| Edizione | [1st edition] |
| Pubbl/distr/stampa | Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 |
| Descrizione fisica | 1 online resource (710 p.) |
| Disciplina | 511.3 |
| Soggetto topico |
Temporal automata
Logic, Symbolic and mathematical |
| ISBN |
1-119-99146-3
1-283-40534-2 9786613405340 1-119-99148-X 1-119-99147-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Cover; Title Page; Copyright; Preface; Chapter 1: Introduction; 1.1 Aims of the Book; 1.2 Why Temporal Logic?; 1.3 What is Temporal Logic?; 1.4 Structure of the Book; Chapter 2: Temporal Logic; 2.1 Intuition; 2.2 Syntactic Aspects; 2.3 Semantics; 2.4 Reactive System Properties; 2.5 What is Temporal Logic?; 2.6 Normal Form; 2.7 Büchi Automata and Temporal Logic; 2.8 Advanced Topics; 2.9 Final Exercises; Chapter 3: Specification; 3.1 Describing Simple Behaviours; 3.2 A Semantics of Imperative Programs; 3.3 Linking Specifications; 3.4 Advanced Topics; 3.5 Final Exercises; 3.6 Where to Next?
Chapter 4: Deduction4.1 Temporal Proof; 4.2 Clausal Temporal Resolution; 4.3 The TSPASS System; 4.4 Advanced topics; 4.5 Final Exercises; Chapter 5: Model Checking; 5.1 Algorithmic Verification; 5.2 Automata-Theoretic Model Checking; 5.3 The Spin System; 5.4 Advanced Topics; 5.5 Final Exercises; Chapter 6: Execution; 6.1 From Specifications to Programs; 6.2 METATEM: Executing Temporal Formulae; 6.3 The Concurrent MetateM system; 6.4 Advanced Topics; Chapter 7: Selected Applications; 7.1 Model Checking Programs; 7.2 Security Protocol Analysis; 7.3 Recognizing Temporal Patterns 7.4 Parameterized Systems7.5 Reasoning with Intervals; 7.6 Planning; Chapter 8: Summary; Appendix A: Review of Classical Logic; A.1 Introduction; A.2 Propositional Logic; A.3 Normal Forms; A.4 Propositional Resolution; A.5 Horn Clauses; A.6 First-Order Logic; Appendix B: Solutions to Exercises; B.1 Solutions: Chapter 2; Solutions: Chapter 3; Solutions: Chapter 4; Solutions: Chapter 5; Solutions: Chapter 6; Solutions: Appendix A; References; Index |
| Record Nr. | UNINA-9910809171103321 |
|
Fisher Michael <1962->
|
||
| Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
