检索结果-内蒙古大学图书馆

Annual Symposium on Logic in computer science

作者： J. Esparza A. Kucera R. Mayr Institute for Formal Methods in Computer Science University of Stuttgart Stuttgart Germany Institute for Formal Methods in Computer Science University of Stuttgart Germany Faculty of Informatics Masaryk University Brno Czech Republic Department of Computer Science Albert Ludwigs University of Freiburg Freiburg im Breisgau Germany

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then, we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

关键词： Automata computer science Probabilistic logic Personal digital assistants Informatics Uncertainty Protocols Fault tolerant systems Asynchronous communication Concurrent computing

来源：评论

学校读者我要写书评

暂无评论

Behavioral modeling for mobile agent systems using Petri nets

Behavioral modeling for mobile agent systems using Petri net...

引用

IEEE International Conference on Systems, Man and Cybernetics

作者： A.A. Pouyan S. Reeves Department of Computing Faculty of Engineering University of Birjand Birjand Iran Formal Methods Laboratory Department of Computer Science University of Waikato Hamilton New Zealand

This work presents a formal Petri net-based approach to behaviour modeling for mobile agent systems. Generic agent templates, formalized in Petri net semantics, are proposed to model the components of a distributed mobile agent system. A generic agent template is conceptualized as an entity consisting of a set of actions, a set of rules which govern the agent communications and an event that captures the agent migration. The communication rules determine the Petri net structures which act as connectors in the proposed approach. The behaviour of the mobile agent is linked to both architectural and structural specifications based on system requirements. After providing certain formal definitions we present a theoretical formal model for designing and describing the behaviour of mobile agent systems for distributed asynchronous applications. It supports formal reasoning based on Petri nets.

关键词： Mobile agents Petri nets Distributed computing computer networks Mobile communication Application software computer network management Mobile computing Telecommunication computing Information management

来源：评论

学校读者我要写书评

暂无评论

Process algebraic model of superscalar processor programs for instruction level timing analysis

引用

7th International Conference on Parallel Computing Technologies, PaCT 2003

作者： Yoo, Hee-Jun Choi, Jin-Young Theory and Formal Methods Lab Dept of Computer Science and Engineering Korea University Seoul136-701 Korea Republic of

ISBN: (纸本)3540406735

This paper illustrates a formal technique for describing timing properties and resource constraints of pipelined out of order superscalar processor instructions at a high level. The degree of parallelism depends on the multiplicity of hardware functional units as well as data dependencies among instructions. Thus, the timing properties of a superscalar program are difficult to analyze and predict. We describe how to model the instruction level architecture of a superscalar processor using ACSR and how to derive the temporal behavior of an assembly program using ACSR laws. Our approach is to model superscalar processor registers as ACSR resources, instructions as ACSR processes, and use ACSR priorities to achieve maximum possible instruction-level parallelism. © Springer-Verlag Berlin Heidelberg 2003.

关键词： Program assemblers

来源：评论

学校读者我要写书评

暂无评论

A polynomial-time algorithm for checking consistency of free-choice signal transition graphs

A polynomial-time algorithm for checking consistency of free...

引用

International Conference on Application of Concurrency to System Design

作者： J. Esparza Institute for Formal Methods in Computer Science University of Stuttgart Germany

Signal transition graphs (STGs) are one of the most popular models for the specification of asynchronous circuits. A STG can be implemented if it admits a so-called consistent and complete binary encoding. Checking this is EXPSPACE-hard for arbitrary STGs, and so a lot of attention has been devoted to the subclass of free-choice STGs, which offers a good compromise between expressive power and analyzability. In the last years, polynomial time synthesis techniques have been developed for free-choice STGs, but they assume that the STG has a consistent binary encoding. The first polynomial algorithm for checking consistency is presented here.

关键词： Polynomials Asynchronous circuits Encoding Circuit synthesis Petri nets Signal synthesis computer science Algorithm design and analysis Clocks Energy consumption

来源：评论

学校读者我要写书评

暂无评论

A generic approach to the static analysis of concurrent programs with procedures

引用

International Journal of Foundations of computer science 2003年第4期14卷 551-582页

作者： Bouajjani, Ahmed Esparza, Javier Touili, Tayssir LIAFA University of Paris 7 75251 Paris cedex 5 2 place Jussieu France Institute for Formal Methods in Computer Science University of Stuttgart 70569 Stuttgart Universitätstr. 38 Germany

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras. © 2003 World Scientific Publishing Company.

关键词： abstraction Concurrent programs with procedures Kleene algebras pushdown systems static analysis verification

来源：评论

学校读者我要写书评

暂无评论

An automata-theoretic approach to software verification

引用

Lecture Notes in computer science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2003年 2710卷 21-21页

作者： Esparza, Javier Institute for Formal Methods in Computer Science Software Reliability and Security Group University of Stuttgart Germany

来源：评论

学校读者我要写书评

暂无评论

BMC via on-the-fly determinization

BMC via on-the-fly determinization

引用

BMC'2003, First International Workshop on Bounded Model Checking

作者： Jussila, Toni Heljanko, Keijo Niemelä, Ilkka Helsinki University of Technology Laboratory for Theoretical Computer Science P.O. Box 5400 FIN-02015 HUT Finland University of Stuttgart Institute for Formal Methods in Computer Science Universitätsstr. 38 D-70569 Stuttgart Germany

The paper develops novel bounded model checking (BMC) techniques for labeled transition systems. The aim is to increase the efficiency of BMC by exploiting the inherent concurrency in the product of LTSs in order to cover more executions of the product within a given bound. This is done by considering a non-standard execution model, step executions, where multiple actions can take place simultaneously and where component LTSs are determinized on-the-fly, i.e., a component may be in a set of states in a step instead of in just one as in standard interleaving executions. Step executions can be further restricted to a subclass called process executions without losing reachable states. For bounded model checking of reachability properties of the product of LTSs the paper presents translation schemes from LTSs to a constrained Boolean circuit such that satisfying valuations of the circuit correspond to step (process) executions of the product. The translation schemes have been implemented and some experimental comparisons performed. The results show that the bound needed for step and process executions is in most cases lower than in interleaving executions and that the running time of the model checker using process executions is smaller than using steps. Moreover, the performance compares favorably to a state-of-the-art interleaving BMC implementation in the NuSMV system. © 2003 Published by Elsevier science B.V.

关键词： Mathematical models

来源：评论

学校读者我要写书评

暂无评论

The MODEST modeling tool and its implementation

引用

13th International Conference on Modelling Techniques and Tools for computer Performance Evaluation, TOOLS 2003

作者： Bohnenkamp, Henrik Hermanns, Holger Katoen, Joost-Pieter Klaren, Ric Formal Methods and Tools Group Department of Computer Science University of Twente P.O. Box 217 Enschede7500 AE Netherlands Department of Computer Science Saarland University SaarbrückenD-66123 Germany

ISBN: (纸本)3540408142

This paper is about the tool-suite MOTOR that supports the modeling and analysis of Modest specifications. In particular, we discuss its tool architecture, and the implementation details of the tool components that do already exist, in particular, the parser, the SOS implementation, an interactive simulator, and a state-space generator. As the expressiveness of Modest goes beyond existing notations for realtime as well as probabilistic systems, the implementation of these tool components has a non-trivial intrinsic complexity. © Springer-Verlag Berlin Heidelberg 2003.

关键词： Artificial intelligence

来源：评论

学校读者我要写书评

暂无评论

CardKt: Automated multi-modal deduction on java cards for multi-application security 1st

引用

1st International Workshop on Java Cards, JavaCard 2000

作者： Goré, Rajeev Nguyen, Lan Duy Automated Reasoning Group Computer Sciences Laboratory Res. Sch. Of Inf. Sci. And Eng. Institute of Advanced Studies Australian National University Australia Formal Methods Group Dept. of Computer Science Australian National University Australia

ISBN: (纸本)9783540421672

We describe an implementation of a Java program to perform automated deduction in propositional multi-modal logics on a Java smart card. The tight space limits of Java smart cards make the implementation non-trivial. A potential application is to ensure that applets down-loaded off the internet conform to personalised security permissions stored on the Java card using a security policy encoded in multi-modal logic. In particular, modal logic may be useful to ensure that previously checked "trust" relationships between pre-existing multiple applets on a Java card are not broken by the addition of a new applet. That is, by using multi-modal logic to express notions of permissions and obligations, we can turn the security check into an on-board theorem proving task. Our theorem prover itself could be down-loaded "just in time" to perform the check, and then deleted to free up space on the card once the check has been completed. Our work is thus a "proof of principle" for the application of formal logic to the security of multi-application Java cards. © Springer-Verlag Berlin Heidelberg 2001.

关键词： Security systems

来源：评论

学校读者我要写书评

暂无评论

ETMCC: model checking performability properties of Markov chains

ETMCC: model checking performability properties of Markov ch...

引用

International Conference on Dependable Systems and Networks (DSN)

作者： H. Hermanns J.t-P. Katoen J. Meyer-Kayser M. Siegle Department of Computer Science Universitat des Saarlandes Germany Formal Methods and Tools Group University of Twente Netherlands Department of Computer Science Universität Erlangen Nürnberg Germany

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：