Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines

·
· Cambridge University Press
eBook
392
āļŦāļ™āđ‰āļē
āļ„āļ°āđāļ™āļ™āđāļĨāļ°āļĢāļĩāļ§āļīāļ§āđ„āļĄāđˆāđ„āļ”āđ‰āļĢāļąāļšāļāļēāļĢāļ•āļĢāļ§āļˆāļŠāļ­āļšāļĒāļ·āļ™āļĒāļąāļ™ Â āļ”āļđāļ‚āđ‰āļ­āļĄāļđāļĨāđ€āļžāļīāđˆāļĄāđ€āļ•āļīāļĄ

āđ€āļāļĩāđˆāļĒāļ§āļāļąāļš eBook āđ€āļĨāđˆāļĄāļ™āļĩāđ‰

How can we provide guarantees of behaviours for autonomous systems such as driverless cars? This tutorial text, for professionals, researchers and graduate students, explains how autonomous systems, from intelligent robots to driverless cars, can be programmed in ways that make them amenable to formal verification. The authors review specific definitions, applications and the unique future potential of autonomous systems, along with their impact on safer decisions and ethical behaviour. Topics discussed include the use of rational cognitive agent programming from the Beliefs-Desires-Intentions paradigm to control autonomous systems and the role model-checking in verifying the properties of this decision-making component. Several case studies concerning both the verification of autonomous systems and extensions to the framework beyond the model-checking of agent decision-makers are included, along with complete tutorials for the use of the freely-available verifiable cognitive agent toolkit Gwendolen, written in Java.

āđ€āļāļĩāđˆāļĒāļ§āļāļąāļšāļœāļđāđ‰āđāļ•āđˆāļ‡

Dr Louise Dennis is leader of the Autonomy and Verification research group at the University of Manchester and conference coordinator for the ACM Special Interest Group for Artificial Intelligence. She studied Mathematics and Philosophy at the University of Oxford and received her PhD from the University of Edinburgh in using AI techniques to prove mathematical theorems; her interest in the overlap between Mathematics, Philosophy and Artificial Intelligence has continued ever since. Her current research encompasses the programming of autonomous systems, the development of agent programming languages, reasoning about systems and programs via formal mathematical techniques, and the ethical implications of Artificial Intelligence. Beyond the university setting, Dr Dennis is active in public engagement and spends a lot of time taking Lego Robots into schools to introduce robotics programming to children.

Dr Michael Fisher is a Professor of Computer Science at the University of Manchester. He holds a Royal Academy of Engineering Chair in Emerging Technologies and is a fellow of both the British Computer Society and the Institution of Engineering and Technology. He was previously a Professor of Logic and Computation in the Department of Computing & Mathematics at the Manchester Metropolitan University and a Professor of Computer Science at the University of Liverpool. Dr Fisher's research concerns autonomous systems, particularly software engineering, formal verification, safety, responsibility, and trustworthiness. He has been involved in over 200 journal and conference papers and authored the book An Introduction to Practical Formal Methods using Temporal Logic (Wiley) in 2011.

āđƒāļŦāđ‰āļ„āļ°āđāļ™āļ™ eBook āļ™āļĩāđ‰

āđāļŠāļ”āļ‡āļ„āļ§āļēāļĄāđ€āļŦāđ‡āļ™āļ‚āļ­āļ‡āļ„āļļāļ“āđƒāļŦāđ‰āđ€āļĢāļēāļĢāļąāļšāļĢāļđāđ‰

āļ‚āđ‰āļ­āļĄāļđāļĨāđƒāļ™āļāļēāļĢāļ­āđˆāļēāļ™

āļŠāļĄāļēāļĢāđŒāļ—āđ‚āļŸāļ™āđāļĨāļ°āđāļ—āđ‡āļšāđ€āļĨāđ‡āļ•
āļ•āļīāļ”āļ•āļąāđ‰āļ‡āđāļ­āļ› Google Play Books āļŠāļģāļŦāļĢāļąāļš Android āđāļĨāļ° iPad/iPhone āđāļ­āļ›āļˆāļ°āļ‹āļīāļ‡āļ„āđŒāđ‚āļ”āļĒāļ­āļąāļ•āđ‚āļ™āļĄāļąāļ•āļīāļāļąāļšāļšāļąāļāļŠāļĩāļ‚āļ­āļ‡āļ„āļļāļ“ āđāļĨāļ°āļŠāđˆāļ§āļĒāđƒāļŦāđ‰āļ„āļļāļ“āļ­āđˆāļēāļ™āđāļšāļšāļ­āļ­āļ™āđ„āļĨāļ™āđŒāļŦāļĢāļ·āļ­āļ­āļ­āļŸāđ„āļĨāļ™āđŒāđ„āļ”āđ‰āļ—āļļāļāļ—āļĩāđˆ
āđāļĨāđ‡āļ›āļ—āđ‡āļ­āļ›āđāļĨāļ°āļ„āļ­āļĄāļžāļīāļ§āđ€āļ•āļ­āļĢāđŒ
āļ„āļļāļ“āļŸāļąāļ‡āļŦāļ™āļąāļ‡āļŠāļ·āļ­āđ€āļŠāļĩāļĒāļ‡āļ—āļĩāđˆāļ‹āļ·āđ‰āļ­āļˆāļēāļ Google Play āđ‚āļ”āļĒāđƒāļŠāđ‰āđ€āļ§āđ‡āļšāđ€āļšāļĢāļēāļ§āđŒāđ€āļ‹āļ­āļĢāđŒāđƒāļ™āļ„āļ­āļĄāļžāļīāļ§āđ€āļ•āļ­āļĢāđŒāđ„āļ”āđ‰
eReader āđāļĨāļ°āļ­āļļāļ›āļāļĢāļ“āđŒāļ­āļ·āđˆāļ™āđ†
āļŦāļēāļāļ•āđ‰āļ­āļ‡āļāļēāļĢāļ­āđˆāļēāļ™āļšāļ™āļ­āļļāļ›āļāļĢāļ“āđŒ e-ink āđ€āļŠāđˆāļ™ Kobo eReader āļ„āļļāļ“āļˆāļ°āļ•āđ‰āļ­āļ‡āļ”āļēāļ§āļ™āđŒāđ‚āļŦāļĨāļ”āđāļĨāļ°āđ‚āļ­āļ™āđ„āļŸāļĨāđŒāđ„āļ›āļĒāļąāļ‡āļ­āļļāļ›āļāļĢāļ“āđŒāļ‚āļ­āļ‡āļ„āļļāļ“ āđ‚āļ›āļĢāļ”āļ—āļģāļ•āļēāļĄāļ§āļīāļ˜āļĩāļāļēāļĢāļ­āļĒāđˆāļēāļ‡āļĨāļ°āđ€āļ­āļĩāļĒāļ”āđƒāļ™āļĻāļđāļ™āļĒāđŒāļŠāđˆāļ§āļĒāđ€āļŦāļĨāļ·āļ­āđ€āļžāļ·āđˆāļ­āđ‚āļ­āļ™āđ„āļŸāļĨāđŒāđ„āļ›āļĒāļąāļ‡ eReader āļ—āļĩāđˆāļĢāļ­āļ‡āļĢāļąāļš