Since 2002, FoLLI awards an annual prize for an outstanding dissertation in the fields of Logic, Language, and Information. This book is based on the Ph.D. thesis of Gabriele Puppis, who was the winner of the E.W. Beth dissertation award for 2007. Puppis' thesis focuses on Logic and Computation and, more specifically, on automata-based decidability techniques for time granularity and on a new method for deciding Monadic Second Order theories of trees. The results presented represent a significant step towards a better understanding of the changes in granularity levels that humans make so easily in cognition of time, space, and other phenomena, whereas their logical and computational structure poses difficult conceptual and computational challenges.

The name "temporal logic" may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts - highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems. Fisher begins with a full introduction to the subject, covering the basics of temporal logic and using a variety of examples, exercises and pointers to more advanced work to help clarify and illustrate the topics discussed. He goes on to describe how this logic can be used to specify a variety of computational systems, looking at issues of linking specifications, concurrency, communication and composition ability. He then analyses temporal specification techniques such as deductive verification, algorithmic verification, and direct execution to develop and verify computational systems. The final chapter on case studies analyses the potential problems that can occur in a range of engineering applications in the areas of robotics, railway signalling, hardware design, ubiquitous computing, intelligent agents, and information security, and explains how temporal logic can improve their accuracy and reliability. Models temporal notions and uses them to analyze computational systems Provides a broad approach to temporal logic across many formal methods - including specification, verification and implementation Introduces and explains freely available tools based on temporal logics and shows how these can be applied Presents exercises and pointers to further study in each chapter, as well as an accompanying website providing links to additional systems based upon temporal logic as well as additional material related to the book.

Handbook of Knowledge Representation describes the essential foundations of Knowledge Representation, which lies at the core of Artificial Intelligence (AI). The book provides an up-to-date review of twenty-five key topics in knowledge representation, written by the leaders of each field. It includes a tutorial background and cutting-edge developments, as well as applications of Knowledge Representation in a variety of AI systems. This handbook is organized into three parts. Part I deals with general methods in Knowledge Representation and reasoning and covers such topics as classical logic in Knowledge Representation; satisfiability solvers; description logics; constraint programming; conceptual graphs; nonmonotonic reasoning; model-based problem solving; and Bayesian networks. Part II focuses on classes of knowledge and specialized representations, with chapters on temporal representation and reasoning; spatial and physical reasoning; reasoning about knowledge and belief; temporal action logics; and nonmonotonic causal logic. Part III discusses Knowledge Representation in applications such as question answering; the semantic web; automated planning; cognitive robotics; multi-agent systems; and knowledge engineering. This book is an essential resource for graduate students, researchers, and practitioners in knowledge representation and AI. * Make your computer smarter* Handle qualitative and uncertain information* Improve computational tractability to solve your problems easily

Centered around 20 major topic areas of both theoretical and practical importance, the World Congress on Neural Networks provides its registrants -- from a diverse background encompassing industry, academia, and government -- with the latest research and applications in the neural network field.

The concept of CAST as Computer Aided Systems Theory, was introduced by F. Pichler in the late 1980s to include those computer theoretical and practical developments as tools to solve problems in System Science. It was considered as the third component (the other two being CAD and CAM) necessary to build the path from Computer and Systems Sciences to practical developments in Science and Engineering. The University of Linz organized the first CAST workshop in April 1988, which demonstrated the acceptance of the concepts by the scientific and technical community. Next, the University of Las Palmas de Gran Canaria joined the University of Linz to organize the first international meeting on CAST, (Las Palmas, February 1989), under the name EUROCAST’89. This was a very successful gathering of systems theorists, computer scientists, and engineers from most European countries, North America, and Japan. It was agreed that EUROCAST international conferences would be organized every two years, alternating between Las Palmas de Gran Canaria and a continental European location. Thus, successive EUROCAST meetings have taken place in Krems (1991), Las Palmas (1993), Innsbruck (1995), Las Palmas (1997), and Vienna (1999), in addition to an extra-European CAST Conference in Ottawa in 1994.

From its early beginnings in the fifties and sixties the field of neural networks has been steadily growing. The first wave was driven by a handful of pioneers who first discovered analogies between machines and biological systems in communication, control and computing. Technological constraints held back research considerably, but gradually computers have become less expensive and more accessible and software tools inceasingly more powerful. Mathematical techniques, developed by computer-aware people, have steadily accumulated and the second wave has begun. Researchers from such diverse areas as psychology, mathematics, physics, neuroscience and engineering now work together in the neural networking field.

New research on the adaptive behavior of natural and synthetic agents.

The present volume contains the proceedings of the 5th International Workshop on Formal Aspects in Security and Trust (FAST 2008), held in Malaga, Spain, October 9-10, 2008. FAST is an event a?liated with the 13th European Sym- sium on Research in Computer Security (ESORICS 2008). FAST 2008 was held under the auspices of the IFIP WG 1.7 on Foundations of Security Analysis and Design. The 5th International Workshop on Formal Aspects in Security and Trust (FAST 2008) aimed at continuing the successful e?ort of the previous three FAST workshop editions for fostering the cooperation among researchers in the areas of security and trust. As computing and network infrastructures become increasingly pervasive, and as they carry increasing economic activity, society needs well-matched security and trust mechanisms. These interactions incre- ingly span several enterprises and involve loosely structured communities of - dividuals. Participants in these activities must control interactions with their partners based on trust policies and business logic. Trust-based decisions - fectively determine the security goals for shared information and for access to sensitive or valuable resources. FAST sought for original papers focusing on formal aspects in: security and trust policy models; security protocol design and analysis; formal models of trustand reputation;logicsfor security andtrust;distributed trust management systems;trust-basedreasoning;digitalassetsprotection;dataprotection;privacy and ID issues; information ?ow analysis; language-based security; security and trust aspects in ubiquitous computing; validation/analysis tools; Web service security/trust/privacy; GRID security; security risk assessment; case studies.

Abstract: "In the past few years, several methods and tools based on process calculi have been developed for verifying properties of concurrent and communicating systems. In this dissertation the interactive theorem prover HOL is used as a framework for supporting reasoning about process calculi based on all the various components of their formal theory. The aim is to build a sound and effective tool to allow both verification of process specifications and meta-theoretic reasoning. In particular, the process calculus CCS is embedded in the HOL logic. This is achieved by first addressing the pure subset of this calculus (no value passing) and then extending it to its value-passing version. The CCS theory is mechanised in HOL by following a purely definitional approach. This means that new objects are embedded in HOL using definition mechanisms which guarantee that no inconsistencies are introduced in the logic, and by deriving new facts from definitions and/or previously proved theorems by formal proof. Pure CCS agent expressions are encoded as a type in the HOL logic, in which initially actions are represented as strings, agents with infinite behaviour are given through the rec-notation and agent summation is the usual binary operator. Recursive agents are then allowed to be defined through systems of recursive equations and to be parameterised. This makes the type of CCS expressions polymorphic and parameterised on the parameters' type. Operational and behavioural semantics and a modal logic are defined and their properties and laws derived in HOL. Several proof tools, such as inference rules, conversions and tactics, are developed to enable users to carry out their proofs in an interactive way and to automate them whenever possible. Properties of infinite state systems, e.g. a counter which can expand indefinitely, can be formally verified in the resulting proof environment. Then, value-passing CCS is mechanised in HOL by translating value-passing expressions into pure ones. This entails a more general polymorphic type for pure agent expressions that includes an indexed summation operator. The translation is proved to be correct with respect to the semantics of value-passing CCS and then used at meta-level, together with the HOL formalisation for pure CCS, for developing behavioural theories for the value-passing calculus. A proof environment is thus derived, in which users will directly work on value-passing specifications. A verification example illustrates how proofs about the data are neatly separated from proofs about the process behaviour and how [omega]-data-rules can be used in a practical way to reason about value- passing agents defined over an infinite value domain."